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/rule_insts.ML
changeset 30763 6976521b4263
parent 30722 623d4831c8cf
child 31945 d5f186aa0bed 
--- a/src/Pure/Isar/rule_insts.ML	Sat Mar 28 17:21:49 2009 +0100
+++ b/src/Pure/Isar/rule_insts.ML	Sat Mar 28 17:53:33 2009 +0100
@@ -283,7 +283,7 @@
         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
isabelle