src/Pure/Isar/proof.ML
changeset 62773 e6443edaebff
parent 62771 dd2914250ca7
child 62819 d3ff367a16a0
     1.1 --- a/src/Pure/Isar/proof.ML	Wed Mar 30 22:35:41 2016 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Wed Mar 30 23:32:50 2016 +0200
     1.3 @@ -600,7 +600,7 @@
     1.4        let
     1.5          val ctxt' =
     1.6            ctxt |> is_none (Variable.default_type ctxt x) ?
     1.7 -            Variable.declare_constraints (Free (x, Mixfix.mixfixT mx));
     1.8 +            Variable.declare_constraints (Free (x, Proof_Context.default_constraint ctxt mx));
     1.9          val t = Free (#1 (Proof_Context.inferred_param x ctxt'));
    1.10        in ((t, mx), ctxt') end
    1.11    | t => ((t, mx), ctxt));