--- a/src/Pure/Tools/rule_insts.ML Sun Mar 29 16:01:12 2015 +0200
+++ b/src/Pure/Tools/rule_insts.ML Sun Mar 29 16:22:35 2015 +0200
@@ -209,7 +209,8 @@
(* goal context *)
-val schematic = Attrib.setup_config_bool @{binding rule_insts_schematic} (K true);
+(*legacy*)
+val schematic = Attrib.setup_config_bool @{binding rule_insts_schematic} (K false);
fun goal_context goal ctxt =
let
@@ -232,7 +233,7 @@
val paramTs = map #2 params;
- (* local fixes and instantiation *)
+ (* instantiation context *)
val ((inst_tvars, inst_vars), inst_ctxt) = goal_ctxt
|> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2