--- a/NEWS Sun Mar 29 16:01:12 2015 +0200
+++ b/NEWS Sun Mar 29 16:22:35 2015 +0200
@@ -61,15 +61,19 @@
*** Pure ***
-* Proof methods with explicit instantiation ("rule_tac", "subgoal_tac"
-etc.) allow an optional context of local variables ('for' declaration):
-these variables become schematic in the instantiated theorem. This
-behaviour is analogous to 'for' in attributes "where" and "of".
-
* Explicit instantiation via attributes "where", "of", and proof methods
"rule_tac" with derivatives like "subgoal_tac" etc. admit dummy patterns
("_") that stand for anonymous local variables.
+* Proof methods with explicit instantiation ("rule_tac", "subgoal_tac"
+etc.) allow an optional context of local variables ('for' declaration):
+these variables become schematic in the instantiated theorem; this
+behaviour is analogous to 'for' in attributes "where" and "of".
+Configuration option rule_insts_schematic (default false) controls use
+of schematic variables outside the context. Minor INCOMPATIBILITY,
+declare rule_insts_schematic = true temporarily and update to use local
+variable declarations or dummy patterns instead.
+
* Configuration option "rule_insts_schematic" determines whether proof
methods like "rule_tac" may refer to undeclared schematic variables
implicitly, instead of using proper 'for' declarations. This historic
--- 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