src/Pure/Isar/rule_insts.ML

           (*the same name are renamed during printing*)
 
         val (param_names, ctxt') = ctxt
           |> Variable.declare_thm thm
           |> Thm.fold_terms Variable.declare_constraints st
-          |> ProofContext.add_fixes_i (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params);
+          |> ProofContext.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params);
 
         (* Process type insts: Tinsts_env *)
         fun absent xi = error
               ("No such variable in theorem: " ^ Term.string_of_vname xi);
         val (rtypes, rsorts) = Drule.types_sorts thm;