src/Pure/Isar/rule_insts.ML
changeset 30763 6976521b4263
parent 30722 623d4831c8cf
child 31945 d5f186aa0bed
     1.1 --- a/src/Pure/Isar/rule_insts.ML	Sat Mar 28 17:21:49 2009 +0100
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Sat Mar 28 17:53:33 2009 +0100
     1.3 @@ -283,7 +283,7 @@
     1.4          val (param_names, ctxt') = ctxt
     1.5            |> Variable.declare_thm thm
     1.6            |> Thm.fold_terms Variable.declare_constraints st
     1.7 -          |> ProofContext.add_fixes_i (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params);
     1.8 +          |> ProofContext.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params);
     1.9  
    1.10          (* Process type insts: Tinsts_env *)
    1.11          fun absent xi = error