Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/proof.ML
changeset 62959 19c2a58623ed
parent 62819 d3ff367a16a0
child 62992 d2e3b3b159d7 
--- a/src/Pure/Isar/proof.ML	Tue Apr 12 14:38:57 2016 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Apr 12 14:50:53 2016 +0200
@@ -600,7 +600,7 @@
       let
         val ctxt' =
           ctxt |> is_none (Variable.default_type ctxt x) ?
-            Variable.declare_constraints (Free (x, Proof_Context.default_constraint ctxt mx));
+            Variable.declare_constraints (Free (x, Mixfix.default_constraint mx));
         val t = Free (#1 (Proof_Context.inferred_param x ctxt'));
       in ((t, mx), ctxt') end
   | t => ((t, mx), ctxt));
isabelle