Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Fri, 20 Mar 2015 22:35:37 +0100
changeset 59772 e6f0c361ac73
parent 59771 c6e60787ffe2
child 59773 3adf5d1c02f6
tuned;
src/Pure/Tools/rule_insts.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Tools/rule_insts.ML	Fri Mar 20 22:18:40 2015 +0100
+++ b/src/Pure/Tools/rule_insts.ML	Fri Mar 20 22:35:37 2015 +0100
@@ -207,14 +207,13 @@
     val (param_names, ctxt') = ctxt
       |> Variable.declare_thm thm
       |> Thm.fold_terms Variable.declare_constraints st
-      |> Proof_Context.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params);
+      |> Proof_Context.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params)
+      ||> Proof_Context.set_mode Proof_Context.mode_schematic;
 
 
     (* lift and instantiate rule *)
 
-    val (inst_tvars, inst_vars) =
-      read_insts (Proof_Context.set_mode Proof_Context.mode_schematic ctxt')
-        mixed_insts thm;
+    val (inst_tvars, inst_vars) = read_insts ctxt' mixed_insts thm;
 
     val maxidx = Thm.maxidx_of st;
     val paramTs = map #2 params;
isabelle