# HG changeset patch # User wenzelm # Date 1390683967 -3600 # Node ID 04448228381de3b493d3a47a0b57bc48d5d8fb9f # Parent 378ae9e4617501d1d877566dd05ec42af64de7d3 explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac; diff -r 378ae9e46175 -r 04448228381d NEWS --- a/NEWS Sat Jan 25 21:52:04 2014 +0100 +++ b/NEWS Sat Jan 25 22:06:07 2014 +0100 @@ -40,6 +40,10 @@ *** Pure *** +* Attributes "where" and "of" allow an optional context of local +variables ('for' declaration): these variables become schematic in the +instantiated theorem. + * More thorough check of proof context for goal statements and attributed fact expressions (concerning background theory, declared hyps). Potential INCOMPATIBILITY, tools need to observe standard @@ -269,6 +273,13 @@ *** ML *** +* Proper context discipline for read_instantiate and instantiate_tac: +variables that are meant to become schematic need to be given as +fixed, and are generalized by the explicit context of local variables. +This corresponds to Isar attributes "where" and "of" with 'for' +declaration. INCOMPATIBILITY, also due to potential change of indices +of schematic variables. + * Toplevel function "use" refers to raw ML bootstrap environment, without Isar context nor antiquotations. Potential INCOMPATIBILITY. Note that 'ML_file' is the canonical command to load ML files into the diff -r 378ae9e46175 -r 04448228381d src/Doc/IsarRef/Proof.thy --- a/src/Doc/IsarRef/Proof.thy Sat Jan 25 21:52:04 2014 +0100 +++ b/src/Doc/IsarRef/Proof.thy Sat Jan 25 22:06:07 2014 +0100 @@ -721,11 +721,13 @@ ; @@{attribute OF} @{syntax thmrefs} ; - @@{attribute of} @{syntax insts} ('concl' ':' @{syntax insts})? + @@{attribute of} @{syntax insts} ('concl' ':' @{syntax insts})? \ + (@'for' (@{syntax vars} + @'and'))? ; @@{attribute "where"} ((@{syntax name} | @{syntax var} | @{syntax typefree} | @{syntax typevar}) '=' - (@{syntax type} | @{syntax term}) * @'and') + (@{syntax type} | @{syntax term}) * @'and') \ + (@'for' (@{syntax vars} + @'and'))? \} \begin{description} @@ -812,6 +814,10 @@ left to right; ``@{text _}'' (underscore) indicates to skip a position. Arguments following a ``@{text "concl:"}'' specification refer to positions of the conclusion of a rule. + + An optional context of local variables @{text "\ x\<^sub>1 \ x\<^sub>m"} may + be specified: the instantiated theorem is exported, and these + variables become schematic (usually with some shifting of indices). \item @{attribute "where"}~@{text "x\<^sub>1 = t\<^sub>1 \ \ x\<^sub>n = t\<^sub>n"} performs named instantiation of schematic type and term variables @@ -821,6 +827,9 @@ As type instantiations are inferred from term instantiations, explicit type instantiations are seldom necessary. + An optional context of local variables @{text "\ x\<^sub>1 \ x\<^sub>m"} may + be specified as for @{attribute "of"} above. + \end{description} *} diff -r 378ae9e46175 -r 04448228381d src/Doc/isar.sty --- a/src/Doc/isar.sty Sat Jan 25 21:52:04 2014 +0100 +++ b/src/Doc/isar.sty Sat Jan 25 22:06:07 2014 +0100 @@ -11,6 +11,7 @@ \newcommand{\indexouternonterm}[1]{\indexdef{}{syntax}{#1}} \newcommand{\indexisarelem}[1]{\indexdef{}{element}{#1}} +\newcommand{\isasymFOR}{\isakeyword{for}} \newcommand{\isasymAND}{\isakeyword{and}} \newcommand{\isasymIS}{\isakeyword{is}} \newcommand{\isasymWHERE}{\isakeyword{where}} diff -r 378ae9e46175 -r 04448228381d src/HOL/Bali/AxExample.thy --- a/src/HOL/Bali/AxExample.thy Sat Jan 25 21:52:04 2014 +0100 +++ b/src/HOL/Bali/AxExample.thy Sat Jan 25 22:06:07 2014 +0100 @@ -41,9 +41,9 @@ declare lvar_def [simp] ML {* -fun inst1_tac ctxt s t st = +fun inst1_tac ctxt s t xs st = case AList.lookup (op =) (rev (Term.add_var_names (Thm.prop_of st) [])) s of - SOME i => instantiate_tac ctxt [((s, i), t)] st | NONE => Seq.empty; + SOME i => instantiate_tac ctxt [((s, i), t)] xs st | NONE => Seq.empty; val ax_tac = REPEAT o rtac allI THEN' @@ -64,7 +64,7 @@ apply (tactic "ax_tac 1" (* Try *)) defer apply (tactic {* inst1_tac @{context} "Q" - "\Y s Z. arr_inv (snd s) \ tprg,s\catch SXcpt NullPointer" *}) + "\Y s Z. arr_inv (snd s) \ tprg,s\catch SXcpt NullPointer" [] *}) prefer 2 apply simp apply (rule_tac P' = "Normal (\Y s Z. arr_inv (snd s))" in conseq1) @@ -83,7 +83,7 @@ apply (tactic "ax_tac 1" (* AVar *)) prefer 2 apply (rule ax_subst_Val_allI) -apply (tactic {* inst1_tac @{context} "P'" "\a. Normal (?PP a\?x)" *}) +apply (tactic {* inst1_tac @{context} "P'" "\a. Normal (PP a\x)" ["PP", "x"] *}) apply (simp del: avar_def2 peek_and_def2) apply (tactic "ax_tac 1") apply (tactic "ax_tac 1") @@ -124,7 +124,7 @@ apply (tactic "ax_tac 1") (* Ass *) prefer 2 apply (rule ax_subst_Var_allI) -apply (tactic {* inst1_tac @{context} "P'" "\a vs l vf. ?PP a vs l vf\?x \. ?p" *}) +apply (tactic {* inst1_tac @{context} "P'" "\a vs l vf. PP a vs l vf\x \. p" ["PP", "x", "p"] *}) apply (rule allI) apply (tactic {* simp_tac (@{context} delloop "split_all_tac" delsimps [@{thm peek_and_def2}, @{thm heap_def2}, @{thm subst_res_def2}, @{thm normal_def2}]) 1 *}) apply (rule ax_derivs.Abrupt) @@ -132,17 +132,17 @@ apply (tactic "ax_tac 1" (* FVar *)) apply (tactic "ax_tac 2", tactic "ax_tac 2", tactic "ax_tac 2") apply (tactic "ax_tac 1") -apply (tactic {* inst1_tac @{context} "R" "\a'. Normal ((\Vals:vs (x, s) Z. arr_inv s \ inited Ext (globs s) \ a' \ Null \ vs = [Null]) \. heap_free two)" *}) +apply (tactic {* inst1_tac @{context} "R" "\a'. Normal ((\Vals:vs (x, s) Z. arr_inv s \ inited Ext (globs s) \ a' \ Null \ vs = [Null]) \. heap_free two)" [] *}) apply fastforce prefer 4 apply (rule ax_derivs.Done [THEN conseq1],force) apply (rule ax_subst_Val_allI) -apply (tactic {* inst1_tac @{context} "P'" "\a. Normal (?PP a\?x)" *}) +apply (tactic {* inst1_tac @{context} "P'" "\a. Normal (PP a\x)" ["PP", "x"] *}) apply (simp (no_asm) del: peek_and_def2 heap_free_def2 normal_def2 o_apply) apply (tactic "ax_tac 1") prefer 2 apply (rule ax_subst_Val_allI) -apply (tactic {* inst1_tac @{context} "P'" "\aa v. Normal (?QQ aa v\?y)" *}) +apply (tactic {* inst1_tac @{context} "P'" "\aa v. Normal (QQ aa v\y)" ["QQ", "y"] *}) apply (simp del: peek_and_def2 heap_free_def2 normal_def2) apply (tactic "ax_tac 1") apply (tactic "ax_tac 1") @@ -161,7 +161,7 @@ apply (tactic "ax_tac 1") defer apply (rule ax_subst_Var_allI) -apply (tactic {* inst1_tac @{context} "P'" "\vf. Normal (?PP vf \. ?p)" *}) +apply (tactic {* inst1_tac @{context} "P'" "\vf. Normal (PP vf \. p)" ["PP", "p"] *}) apply (simp (no_asm) del: split_paired_All peek_and_def2 initd_def2 heap_free_def2 normal_def2) apply (tactic "ax_tac 1" (* NewC *)) apply (tactic "ax_tac 1" (* ax_Alloc *)) @@ -189,18 +189,18 @@ apply (tactic "ax_tac 1") apply (tactic "ax_tac 1") apply (rule_tac [2] ax_subst_Var_allI) -apply (tactic {* inst1_tac @{context} "P'" "\vf l vfa. Normal (?P vf l vfa)" *}) +apply (tactic {* inst1_tac @{context} "P'" "\vf l vfa. Normal (P vf l vfa)" ["P"] *}) apply (tactic {* simp_tac (@{context} delloop "split_all_tac" delsimps [@{thm split_paired_All}, @{thm peek_and_def2}, @{thm heap_free_def2}, @{thm initd_def2}, @{thm normal_def2}, @{thm supd_lupd}]) 2 *}) apply (tactic "ax_tac 2" (* NewA *)) apply (tactic "ax_tac 3" (* ax_Alloc_Arr *)) apply (tactic "ax_tac 3") -apply (tactic {* inst1_tac @{context} "P" "\vf l vfa. Normal (?P vf l vfa\\)" *}) +apply (tactic {* inst1_tac @{context} "P" "\vf l vfa. Normal (P vf l vfa\\)" ["P"] *}) apply (tactic {* simp_tac (@{context} delloop "split_all_tac") 2 *}) apply (tactic "ax_tac 2") apply (tactic "ax_tac 1" (* FVar *)) apply (tactic "ax_tac 2" (* StatRef *)) apply (rule ax_derivs.Done [THEN conseq1]) -apply (tactic {* inst1_tac @{context} "Q" "\vf. Normal ((\Y s Z. vf=lvar (VName e) (snd s)) \. heap_free four \. initd Base \. initd Ext)" *}) +apply (tactic {* inst1_tac @{context} "Q" "\vf. Normal ((\Y s Z. vf=lvar (VName e) (snd s)) \. heap_free four \. initd Base \. initd Ext)" [] *}) apply (clarsimp split del: split_if) apply (frule atleast_free_weaken [THEN atleast_free_weaken]) apply (drule initedD) @@ -210,9 +210,9 @@ apply (rule ax_triv_Init_Object [THEN peek_and_forget2, THEN conseq1]) apply (rule wf_tprg) apply clarsimp -apply (tactic {* inst1_tac @{context} "P" "\vf. Normal ((\Y s Z. vf = lvar (VName e) (snd s)) \. heap_free four \. initd Ext)" *}) +apply (tactic {* inst1_tac @{context} "P" "\vf. Normal ((\Y s Z. vf = lvar (VName e) (snd s)) \. heap_free four \. initd Ext)" [] *}) apply clarsimp -apply (tactic {* inst1_tac @{context} "PP" "\vf. Normal ((\Y s Z. vf = lvar (VName e) (snd s)) \. heap_free four \. Not \ initd Base)" *}) +apply (tactic {* inst1_tac @{context} "PP" "\vf. Normal ((\Y s Z. vf = lvar (VName e) (snd s)) \. heap_free four \. Not \ initd Base)" [] *}) apply clarsimp (* end init *) apply (rule conseq1) @@ -244,7 +244,7 @@ apply clarsimp apply (tactic "ax_tac 1" (* If *)) apply (tactic - {* inst1_tac @{context} "P'" "Normal (\s.. (\Y s Z. True)\=Val (the (locals s i)))" *}) + {* inst1_tac @{context} "P'" "Normal (\s.. (\Y s Z. True)\=Val (the (locals s i)))" [] *}) apply (tactic "ax_tac 1") apply (rule conseq1) apply (tactic "ax_tac 1") @@ -265,7 +265,7 @@ apply (tactic "ax_tac 1") prefer 2 apply (rule ax_subst_Var_allI) -apply (tactic {* inst1_tac @{context} "P'" "\b Y ba Z vf. \Y (x,s) Z. x=None \ snd vf = snd (lvar i s)" *}) +apply (tactic {* inst1_tac @{context} "P'" "\b Y ba Z vf. \Y (x,s) Z. x=None \ snd vf = snd (lvar i s)" [] *}) apply (rule allI) apply (rule_tac P' = "Normal ?P" in conseq1) prefer 2 diff -r 378ae9e46175 -r 04448228381d src/HOL/Bali/Basis.thy --- a/src/HOL/Bali/Basis.thy Sat Jan 25 21:52:04 2014 +0100 +++ b/src/HOL/Bali/Basis.thy Sat Jan 25 22:06:07 2014 +0100 @@ -181,7 +181,7 @@ ML {* fun sum3_instantiate ctxt thm = map (fn s => simplify (ctxt delsimps [@{thm not_None_eq}]) - (read_instantiate ctxt [(("t", 0), "In" ^ s ^ " ?x")] thm)) ["1l","2","3","1r"] + (read_instantiate ctxt [(("t", 0), "In" ^ s ^ " x")] ["x"] thm)) ["1l","2","3","1r"] *} (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *) diff -r 378ae9e46175 -r 04448228381d src/HOL/Library/Binomial.thy --- a/src/HOL/Library/Binomial.thy Sat Jan 25 21:52:04 2014 +0100 +++ b/src/HOL/Library/Binomial.thy Sat Jan 25 22:06:07 2014 +0100 @@ -131,7 +131,7 @@ prefer 4 apply (force simp add: constr_bij) prefer 3 apply force prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2] - finite_subset [of _ "Pow (insert x F)", standard]) + finite_subset [of _ "Pow (insert x F)" for F]) apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset]) done qed diff -r 378ae9e46175 -r 04448228381d src/HOL/Number_Theory/Binomial.thy --- a/src/HOL/Number_Theory/Binomial.thy Sat Jan 25 21:52:04 2014 +0100 +++ b/src/HOL/Number_Theory/Binomial.thy Sat Jan 25 22:06:07 2014 +0100 @@ -133,7 +133,7 @@ prefer 4 apply (force simp add: constr_bij) prefer 3 apply force prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2] - finite_subset [of _ "Pow (insert x F)", standard]) + finite_subset [of _ "Pow (insert x F)" for F]) apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset]) done qed @@ -669,7 +669,9 @@ have "inj_on snd (SIGMA i:{1..card A}. ?I i)" using assms by(auto intro!: inj_onI) moreover have [symmetric]: "snd ` (SIGMA i:{1..card A}. ?I i) = {I. I \ A \ I \ {} \ x \ \I}" - using assms by(auto intro!: rev_image_eqI[where x="(card a, a)", standard] simp add: card_gt_0_iff[folded Suc_le_eq] dest: finite_subset intro: card_mono) + using assms by(auto intro!: rev_image_eqI[where x="(card a, a)" for a] + simp add: card_gt_0_iff[folded Suc_le_eq] + dest: finite_subset intro: card_mono) ultimately have "?lhs x = (\(i, I)\(SIGMA i:{1..card A}. ?I i). -1 ^ (i + 1))" by(rule setsum_reindex_cong[where f=snd]) fastforce also have "\ = (\i=1..card A. (\I|I \ A \ card I = i \ x \ \I. -1 ^ (i + 1)))" diff -r 378ae9e46175 -r 04448228381d src/HOL/Prolog/prolog.ML --- a/src/HOL/Prolog/prolog.ML Sat Jan 25 21:52:04 2014 +0100 +++ b/src/HOL/Prolog/prolog.ML Sat Jan 25 22:06:07 2014 +0100 @@ -49,14 +49,16 @@ fun check_HOHH thm = (if isD (concl_of thm) andalso forall isG (prems_of thm) then thm else raise not_HOHH); -fun atomizeD ctxt thm = let +fun atomizeD ctxt thm = + let fun at thm = case concl_of thm of - _$(Const(@{const_name All} ,_)$Abs(s,_,_))=> at(thm RS - (read_instantiate ctxt [(("x", 0), "?" ^ (if s="P" then "PP" else s))] spec)) + _$(Const(@{const_name All} ,_)$Abs(s,_,_))=> + let val s' = if s="P" then "PP" else s + in at(thm RS (read_instantiate ctxt [(("x", 0), s')] [s'] spec)) end | _$(Const(@{const_name HOL.conj},_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2) | _$(Const(@{const_name HOL.implies},_)$_$_) => at(thm RS mp) | _ => [thm] -in map zero_var_indexes (at thm) end; + in map zero_var_indexes (at thm) end; val atomize_ss = (empty_simpset @{context} |> Simplifier.set_mksimps (mksimps mksimps_pairs)) diff -r 378ae9e46175 -r 04448228381d src/HOL/Rat.thy --- a/src/HOL/Rat.thy Sat Jan 25 21:52:04 2014 +0100 +++ b/src/HOL/Rat.thy Sat Jan 25 22:06:07 2014 +0100 @@ -622,8 +622,8 @@ (* not needed because x < (y::int) can be rewritten as x + 1 <= y: of_int_less_iff RS iffD2 *) #> Lin_Arith.add_simps [@{thm neg_less_iff_less}, @{thm True_implies_equals}, - read_instantiate @{context} [(("a", 0), "(numeral ?v)")] @{thm distrib_left}, - read_instantiate @{context} [(("a", 0), "(- numeral ?v)")] @{thm distrib_left}, + @{thm distrib_left [where a = "numeral v" for v]}, + @{thm distrib_left [where a = "- numeral v" for v]}, @{thm divide_1}, @{thm divide_zero_left}, @{thm times_divide_eq_right}, @{thm times_divide_eq_left}, @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym, diff -r 378ae9e46175 -r 04448228381d src/HOL/Set.thy --- a/src/HOL/Set.thy Sat Jan 25 21:52:04 2014 +0100 +++ b/src/HOL/Set.thy Sat Jan 25 22:06:07 2014 +0100 @@ -1577,10 +1577,10 @@ by (auto simp add: Pow_def) lemma Pow_insert: "Pow (insert a A) = Pow A \ (insert a ` Pow A)" - by (blast intro: image_eqI [where ?x = "u - {a}", standard]) + by (blast intro: image_eqI [where ?x = "u - {a}" for u]) lemma Pow_Compl: "Pow (- A) = {-B | B. A \ Pow B}" - by (blast intro: exI [where ?x = "- u", standard]) + by (blast intro: exI [where ?x = "- u" for u]) lemma Pow_UNIV [simp]: "Pow UNIV = UNIV" by blast diff -r 378ae9e46175 -r 04448228381d src/HOL/Set_Interval.thy --- a/src/HOL/Set_Interval.thy Sat Jan 25 21:52:04 2014 +0100 +++ b/src/HOL/Set_Interval.thy Sat Jan 25 22:06:07 2014 +0100 @@ -728,7 +728,7 @@ qed auto lemma image_int_atLeastLessThan: "int ` {a.. hackish_string_of_term ctxt in ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]", - stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)]) + stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)] []) end fun type_match thy (T1, T2) = diff -r 378ae9e46175 -r 04448228381d src/HOL/Tools/TFL/post.ML --- a/src/HOL/Tools/TFL/post.ML Sat Jan 25 21:52:04 2014 +0100 +++ b/src/HOL/Tools/TFL/post.ML Sat Jan 25 22:06:07 2014 +0100 @@ -130,7 +130,7 @@ rule_by_tactic ctxt (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE))); (*Strip off the outer !P*) -val spec'= read_instantiate @{context} [(("x", 0), "P::?'b=>bool")] spec; +val spec'= read_instantiate @{context} [(("x", 0), "P::'b=>bool")] [] spec; fun tracing true _ = () | tracing false msg = writeln msg; diff -r 378ae9e46175 -r 04448228381d src/Pure/Tools/rule_insts.ML --- a/src/Pure/Tools/rule_insts.ML Sat Jan 25 21:52:04 2014 +0100 +++ b/src/Pure/Tools/rule_insts.ML Sat Jan 25 22:06:07 2014 +0100 @@ -6,8 +6,8 @@ signature BASIC_RULE_INSTS = sig - val read_instantiate: Proof.context -> (indexname * string) list -> thm -> thm - val instantiate_tac: Proof.context -> (indexname * string) list -> tactic + val read_instantiate: Proof.context -> (indexname * string) list -> string list -> thm -> thm + val instantiate_tac: Proof.context -> (indexname * string) list -> string list -> tactic val res_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic val eres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic val cut_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic @@ -20,6 +20,10 @@ signature RULE_INSTS = sig include BASIC_RULE_INSTS + val where_rule: Proof.context -> (indexname * string) list -> + (binding * string option * mixfix) list -> thm -> thm + val of_rule: Proof.context -> string option list * string option list -> + (binding * string option * mixfix) list -> thm -> thm val make_elim_preserve: thm -> thm val method: (Proof.context -> (indexname * string) list -> thm -> int -> tactic) -> (Proof.context -> thm list -> int -> tactic) -> (Proof.context -> Proof.method) context_parser @@ -123,9 +127,10 @@ (map (pairself certT) inst_tvars, map (pairself cert) inst_vars) end; -fun read_instantiate_mixed ctxt mixed_insts thm = +fun where_rule ctxt mixed_insts fixes thm = let val ctxt' = ctxt + |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2 |> Variable.declare_thm thm |> fold (fn a => Variable.declare_names (Logic.mk_type (TFree (a, dummyS)))) (add_used thm []); (* FIXME !? *) val tvars = Thm.fold_terms Term.add_tvars thm []; @@ -133,10 +138,11 @@ val insts = read_insts ctxt' mixed_insts (tvars, vars); in Drule.instantiate_normalize insts thm + |> singleton (Proof_Context.export ctxt' ctxt) |> Rule_Cases.save thm end; -fun read_instantiate_mixed' ctxt (args, concl_args) thm = +fun of_rule ctxt (args, concl_args) fixes thm = let fun zip_vars _ [] = [] | zip_vars (_ :: xs) (NONE :: rest) = zip_vars xs rest @@ -145,17 +151,18 @@ val insts = zip_vars (rev (Term.add_vars (Thm.full_prop_of thm) [])) args @ zip_vars (rev (Term.add_vars (Thm.concl_of thm) [])) concl_args; - in read_instantiate_mixed ctxt insts thm end; + in where_rule ctxt insts fixes thm end; end; (* instantiation of rule or goal state *) -fun read_instantiate ctxt = - read_instantiate_mixed (ctxt |> Proof_Context.set_mode Proof_Context.mode_schematic); (* FIXME !? *) +fun read_instantiate ctxt insts xs = + where_rule ctxt insts (map (fn x => (Binding.name x, NONE, NoSyn)) xs); -fun instantiate_tac ctxt args = PRIMITIVE (read_instantiate ctxt args); +fun instantiate_tac ctxt insts fixes = + PRIMITIVE (read_instantiate ctxt insts fixes); @@ -165,9 +172,10 @@ val _ = Theory.setup (Attrib.setup @{binding "where"} - (Scan.lift (Parse.and_list (Args.var -- (Args.$$$ "=" |-- Args.name_inner_syntax))) >> - (fn args => - Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args))) + (Scan.lift + (Parse.and_list (Args.var -- (Args.$$$ "=" |-- Args.name_inner_syntax)) -- Parse.for_fixes) >> + (fn (insts, fixes) => + Thm.rule_attribute (fn context => where_rule (Context.proof_of context) insts fixes))) "named instantiation of theorem"); @@ -186,8 +194,8 @@ val _ = Theory.setup (Attrib.setup @{binding "of"} - (Scan.lift insts >> (fn args => - Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args))) + (Scan.lift (insts -- Parse.for_fixes) >> (fn (args, fixes) => + Thm.rule_attribute (fn context => of_rule (Context.proof_of context) args fixes))) "positional instantiation of theorem"); end; diff -r 378ae9e46175 -r 04448228381d src/ZF/ind_syntax.ML --- a/src/ZF/ind_syntax.ML Sat Jan 25 21:52:04 2014 +0100 +++ b/src/ZF/ind_syntax.ML Sat Jan 25 22:06:07 2014 +0100 @@ -50,7 +50,7 @@ (*For deriving cases rules. CollectD2 discards the domain, which is redundant; read_instantiate replaces a propositional variable by a formula variable*) val equals_CollectD = - read_instantiate @{context} [(("W", 0), "?Q")] + read_instantiate @{context} [(("W", 0), "Q")] ["Q"] (make_elim (@{thm equalityD1} RS @{thm subsetD} RS @{thm CollectD2}));