title: Locale definition produces two parse trees
body: <p>Here is my simple locale definition in Isabelle:</p>
  <pre><code>locale sig =
    fixes le:: &quot;'a ⇒ 'a ⇒ bool&quot; (infixl &quot;≤&quot; 50)
    assumes refl: &quot;x ≤ x&quot;
  </code></pre>
  <p>Now, I get an error message:</p>
  <pre><code>Ambiguous input⌂ produces 2 parse trees:
    (&quot;\&lt;^const&gt;HOL.Trueprop&quot;
      (&quot;\&lt;^const&gt;Orderings.ord_class.less_eq&quot; (&quot;_position&quot; x) (&quot;_position&quot; x)))
    (&quot;\&lt;^const&gt;HOL.Trueprop&quot; (&quot;\&lt;^fixed&gt;le&quot; (&quot;_position&quot; x) (&quot;_position&quot; x)))
  Ambiguous input
  2 terms are type correct:
    (x ≤ x)
    (x ≤ x)
  Failed to parse prop
  </code></pre>
  <p>Do I have a conflict with a builtin less-or-equal operator?</p>
  <p>How can I fix this?</p>