# 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;