# HG changeset patch
# User wenzelm
# Date 1426887337 -3600
# Node ID e6f0c361ac731c79479c0b9cc92580ced3e239ff
# Parent  c6e60787ffe2f405fd597f2025f16068c2a29566
tuned;

diff -r c6e60787ffe2 -r e6f0c361ac73 src/Pure/Tools/rule_insts.ML
--- 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;