pervasive RuleInsts;
authorwenzelm
Mon Jun 16 22:13:39 2008 +0200 (2008-06-16)
changeset 27239f2f42f9fa09d
parent 27238 d2bf12727c8a
child 27240 1caa6726168a
pervasive RuleInsts;
doc-src/IsarRef/Thy/Generic.thy
doc-src/IsarRef/Thy/ML_Tactic.thy
doc-src/TutorialI/Protocol/Message.thy
src/CCL/CCL.thy
src/CCL/Hered.thy
src/CCL/Wfd.thy
src/CTT/CTT.thy
src/FOL/FOL.thy
src/HOL/Auth/Message.thy
src/HOL/Bali/Basis.thy
src/HOL/Bali/WellType.thy
src/HOL/Hyperreal/MacLaurin.thy
src/HOL/IMPP/Hoare.thy
src/HOL/NanoJava/Equivalence.thy
src/HOL/Nominal/nominal_fresh_fun.ML
src/HOL/Prolog/prolog.ML
src/HOL/Real/rat_arith.ML
src/HOL/SET-Protocol/MessageSET.thy
src/HOL/TLA/TLA.thy
src/HOL/Tools/TFL/post.ML
src/HOL/Tools/induct_tacs.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/metis_tools.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/split_rule.ML
src/HOL/UNITY/UNITY_tactics.ML
src/HOLCF/IOA/meta_theory/Sequence.thy
src/HOLCF/Tools/domain/domain_library.ML
src/HOLCF/Tools/domain/domain_theorems.ML
src/LCF/LCF.thy
src/Sequents/LK0.thy
src/ZF/Tools/induct_tacs.ML
src/ZF/UNITY/SubstAx.thy
src/ZF/ind_syntax.ML
     1.1 --- a/doc-src/IsarRef/Thy/Generic.thy	Mon Jun 16 17:56:08 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Generic.thy	Mon Jun 16 22:13:39 2008 +0200
     1.3 @@ -308,7 +308,7 @@
     1.4  
     1.5    \item [@{method rule_tac} etc.] do resolution of rules with explicit
     1.6    instantiation.  This works the same way as the ML tactics @{ML
     1.7 -  Tactic.res_inst_tac} etc. (see \cite[\S3]{isabelle-ref})
     1.8 +  res_inst_tac} etc. (see \cite[\S3]{isabelle-ref})
     1.9  
    1.10    Multiple rules may be only given if there is no instantiation; then
    1.11    @{method rule_tac} is the same as @{ML resolve_tac} in ML (see
    1.12 @@ -323,12 +323,12 @@
    1.13  
    1.14    \item [@{method thin_tac}~@{text \<phi>}] deletes the specified
    1.15    assumption from a subgoal; note that @{text \<phi>} may contain schematic
    1.16 -  variables.  See also @{ML Tactic.thin_tac} in
    1.17 +  variables.  See also @{ML thin_tac} in
    1.18    \cite[\S3]{isabelle-ref}.
    1.19  
    1.20    \item [@{method subgoal_tac}~@{text \<phi>}] adds @{text \<phi>} as an
    1.21 -  assumption to a subgoal.  See also @{ML Tactic.subgoal_tac} and @{ML
    1.22 -  Tactic.subgoals_tac} in \cite[\S3]{isabelle-ref}.
    1.23 +  assumption to a subgoal.  See also @{ML subgoal_tac} and @{ML
    1.24 +  subgoals_tac} in \cite[\S3]{isabelle-ref}.
    1.25  
    1.26    \item [@{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"}] renames
    1.27    parameters of a goal according to the list @{text "x\<^sub>1, \<dots>,
     2.1 --- a/doc-src/IsarRef/Thy/ML_Tactic.thy	Mon Jun 16 17:56:08 2008 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/ML_Tactic.thy	Mon Jun 16 22:13:39 2008 +0200
     2.3 @@ -41,7 +41,7 @@
     2.4    @{ML forward_tac}).
     2.5  
     2.6    \item Optional explicit instantiation (e.g.\ @{ML resolve_tac} vs.\
     2.7 -  @{ML RuleInsts.res_inst_tac}).
     2.8 +  @{ML res_inst_tac}).
     2.9  
    2.10    \item Abbreviations for singleton arguments (e.g.\ @{ML resolve_tac}
    2.11    vs.\ @{ML rtac}).
    2.12 @@ -66,11 +66,11 @@
    2.13    \begin{tabular}{lll}
    2.14      @{ML rtac}~@{text "a 1"} & & @{text "rule a"} \\
    2.15      @{ML resolve_tac}~@{text "[a\<^sub>1, \<dots>] 1"} & & @{text "rule a\<^sub>1 \<dots>"} \\
    2.16 -    @{ML RuleInsts.res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a 1"} & &
    2.17 +    @{ML res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a 1"} & &
    2.18      @{text "rule_tac x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> a"} \\[0.5ex]
    2.19      @{ML rtac}~@{text "a i"} & & @{text "rule_tac [i] a"} \\
    2.20      @{ML resolve_tac}~@{text "[a\<^sub>1, \<dots>] i"} & & @{text "rule_tac [i] a\<^sub>1 \<dots>"} \\
    2.21 -    @{ML RuleInsts.res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a i"} & &
    2.22 +    @{ML res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a i"} & &
    2.23      @{text "rule_tac [i] x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> a"} \\
    2.24    \end{tabular}
    2.25    \medskip
     3.1 --- a/doc-src/TutorialI/Protocol/Message.thy	Mon Jun 16 17:56:08 2008 +0200
     3.2 +++ b/doc-src/TutorialI/Protocol/Message.thy	Mon Jun 16 22:13:39 2008 +0200
     3.3 @@ -864,7 +864,7 @@
     3.4       (EVERY 
     3.5        [  (*push in occurrences of X...*)
     3.6         (REPEAT o CHANGED)
     3.7 -           (RuleInsts.res_inst_tac (Simplifier.the_context ss)
     3.8 +           (res_inst_tac (Simplifier.the_context ss)
     3.9              [(("x", 1), "X")] (insert_commute RS ssubst) 1),
    3.10         (*...allowing further simplifications*)
    3.11         simp_tac ss 1,
     4.1 --- a/src/CCL/CCL.thy	Mon Jun 16 17:56:08 2008 +0200
     4.2 +++ b/src/CCL/CCL.thy	Mon Jun 16 22:13:39 2008 +0200
     4.3 @@ -415,7 +415,7 @@
     4.4  
     4.5  ML {*
     4.6    fun po_coinduct_tac ctxt s i =
     4.7 -    RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm po_coinduct} i
     4.8 +    res_inst_tac ctxt [(("R", 0), s)] @{thm po_coinduct} i
     4.9  *}
    4.10  
    4.11  
    4.12 @@ -460,11 +460,8 @@
    4.13    done
    4.14  
    4.15  ML {*
    4.16 -  fun eq_coinduct_tac ctxt s i =
    4.17 -    RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct} i
    4.18 -
    4.19 -  fun eq_coinduct3_tac ctxt s i =
    4.20 -    RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct3} i
    4.21 +  fun eq_coinduct_tac ctxt s i = res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct} i
    4.22 +  fun eq_coinduct3_tac ctxt s i = res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct3} i
    4.23  *}
    4.24  
    4.25  
     5.1 --- a/src/CCL/Hered.thy	Mon Jun 16 17:56:08 2008 +0200
     5.2 +++ b/src/CCL/Hered.thy	Mon Jun 16 22:13:39 2008 +0200
     5.3 @@ -97,8 +97,7 @@
     5.4    done
     5.5  
     5.6  ML {*
     5.7 -  fun HTT_coinduct_tac ctxt s i =
     5.8 -    RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct} i
     5.9 +  fun HTT_coinduct_tac ctxt s i = res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct} i
    5.10  *}
    5.11  
    5.12  lemma HTT_coinduct3:
    5.13 @@ -111,7 +110,7 @@
    5.14  val HTT_coinduct3_raw = rewrite_rule [@{thm HTTgen_def}] @{thm HTT_coinduct3}
    5.15  
    5.16  fun HTT_coinduct3_tac ctxt s i =
    5.17 -  RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct3} i
    5.18 +  res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct3} i
    5.19  
    5.20  val HTTgenIs =
    5.21    map (mk_genIs @{theory} @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono})
     6.1 --- a/src/CCL/Wfd.thy	Mon Jun 16 17:56:08 2008 +0200
     6.2 +++ b/src/CCL/Wfd.thy	Mon Jun 16 22:13:39 2008 +0200
     6.3 @@ -55,7 +55,7 @@
     6.4  
     6.5  ML {*
     6.6    fun wfd_strengthen_tac ctxt s i =
     6.7 -    RuleInsts.res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac (i+1)
     6.8 +    res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac (i+1)
     6.9  *}
    6.10  
    6.11  lemma wf_anti_sym: "[| Wfd(r);  <a,x>:r;  <x,a>:r |] ==> P"
    6.12 @@ -456,7 +456,7 @@
    6.13  in
    6.14  
    6.15  fun rcall_tac ctxt i =
    6.16 -  let fun tac ps rl i = RuleInsts.res_inst_tac ctxt ps rl i THEN atac i
    6.17 +  let fun tac ps rl i = res_inst_tac ctxt ps rl i THEN atac i
    6.18    in IHinst tac @{thms rcallTs} i end
    6.19    THEN eresolve_tac @{thms rcall_lemmas} i
    6.20  
    6.21 @@ -478,7 +478,7 @@
    6.22                                   hyp_subst_tac)
    6.23  
    6.24  fun clean_ccs_tac ctxt =
    6.25 -  let fun tac ps rl i = RuleInsts.eres_inst_tac ctxt ps rl i THEN atac i in
    6.26 +  let fun tac ps rl i = eres_inst_tac ctxt ps rl i THEN atac i in
    6.27      TRY (REPEAT_FIRST (IHinst tac @{thms hyprcallTs} ORELSE'
    6.28      eresolve_tac ([asm_rl, @{thm SubtypeE}] @ @{thms rmIHs}) ORELSE'
    6.29      hyp_subst_tac))
     7.1 --- a/src/CTT/CTT.thy	Mon Jun 16 17:56:08 2008 +0200
     7.2 +++ b/src/CTT/CTT.thy	Mon Jun 16 22:13:39 2008 +0200
     7.3 @@ -417,13 +417,13 @@
     7.4      The (rtac EqE i) lets them apply to equality judgements. **)
     7.5  
     7.6  fun NE_tac ctxt sp i =
     7.7 -  TRY (rtac @{thm EqE} i) THEN RuleInsts.res_inst_tac ctxt [(("p", 0), sp)] @{thm NE} i
     7.8 +  TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [(("p", 0), sp)] @{thm NE} i
     7.9  
    7.10  fun SumE_tac ctxt sp i =
    7.11 -  TRY (rtac @{thm EqE} i) THEN RuleInsts.res_inst_tac ctxt [(("p", 0), sp)] @{thm SumE} i
    7.12 +  TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [(("p", 0), sp)] @{thm SumE} i
    7.13  
    7.14  fun PlusE_tac ctxt sp i =
    7.15 -  TRY (rtac @{thm EqE} i) THEN RuleInsts.res_inst_tac ctxt [(("p", 0), sp)] @{thm PlusE} i
    7.16 +  TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [(("p", 0), sp)] @{thm PlusE} i
    7.17  
    7.18  (** Predicate logic reasoning, WITH THINNING!!  Procedures adapted from NJ. **)
    7.19  
     8.1 --- a/src/FOL/FOL.thy	Mon Jun 16 17:56:08 2008 +0200
     8.2 +++ b/src/FOL/FOL.thy	Mon Jun 16 22:13:39 2008 +0200
     8.3 @@ -70,8 +70,7 @@
     8.4    done
     8.5  
     8.6  ML {*
     8.7 -  fun case_tac ctxt a =
     8.8 -    RuleInsts.res_inst_tac ctxt [(("P", 0), a)] @{thm case_split}
     8.9 +  fun case_tac ctxt a = res_inst_tac ctxt [(("P", 0), a)] @{thm case_split}
    8.10  *}
    8.11  
    8.12  method_setup case_tac =
     9.1 --- a/src/HOL/Auth/Message.thy	Mon Jun 16 17:56:08 2008 +0200
     9.2 +++ b/src/HOL/Auth/Message.thy	Mon Jun 16 22:13:39 2008 +0200
     9.3 @@ -884,8 +884,7 @@
     9.4       (EVERY 
     9.5        [  (*push in occurrences of X...*)
     9.6         (REPEAT o CHANGED)
     9.7 -           (RuleInsts.res_inst_tac (Simplifier.the_context ss)
     9.8 -              [(("x", 1), "X")] (insert_commute RS ssubst) 1),
     9.9 +           (res_inst_tac (Simplifier.the_context ss) [(("x", 1), "X")] (insert_commute RS ssubst) 1),
    9.10         (*...allowing further simplifications*)
    9.11         simp_tac ss 1,
    9.12         REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
    10.1 --- a/src/HOL/Bali/Basis.thy	Mon Jun 16 17:56:08 2008 +0200
    10.2 +++ b/src/HOL/Bali/Basis.thy	Mon Jun 16 22:13:39 2008 +0200
    10.3 @@ -230,7 +230,7 @@
    10.4  ML {*
    10.5  fun sum3_instantiate ctxt thm = map (fn s =>
    10.6    simplify (Simplifier.local_simpset_of ctxt delsimps[@{thm not_None_eq}])
    10.7 -    (RuleInsts.read_instantiate ctxt [(("t", 0), "In" ^ s ^ " ?x")] thm)) ["1l","2","3","1r"]
    10.8 +    (read_instantiate ctxt [(("t", 0), "In" ^ s ^ " ?x")] thm)) ["1l","2","3","1r"]
    10.9  *}
   10.10  (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
   10.11  
    11.1 --- a/src/HOL/Bali/WellType.thy	Mon Jun 16 17:56:08 2008 +0200
    11.2 +++ b/src/HOL/Bali/WellType.thy	Mon Jun 16 22:13:39 2008 +0200
    11.3 @@ -653,10 +653,11 @@
    11.4  apply (safe del: disjE)
    11.5  (* 17 subgoals *)
    11.6  apply (tactic {* ALLGOALS (fn i =>
    11.7 -  if i = 11 then EVERY'[RuleInsts.thin_tac @{context} "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean",
    11.8 -    RuleInsts.thin_tac @{context} "?E,dt\<Turnstile>e1\<Colon>-?T1",
    11.9 -    RuleInsts.thin_tac @{context} "?E,dt\<Turnstile>e2\<Colon>-?T2"] i
   11.10 -  else RuleInsts.thin_tac @{context} "All ?P" i) *})
   11.11 +  if i = 11 then EVERY'
   11.12 +   [thin_tac @{context} "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean",
   11.13 +    thin_tac @{context} "?E,dt\<Turnstile>e1\<Colon>-?T1",
   11.14 +    thin_tac @{context} "?E,dt\<Turnstile>e2\<Colon>-?T2"] i
   11.15 +  else thin_tac @{context} "All ?P" i) *})
   11.16  (*apply (safe del: disjE elim!: wt_elim_cases)*)
   11.17  apply (tactic {*ALLGOALS (eresolve_tac @{thms wt_elim_cases})*})
   11.18  apply (simp_all (no_asm_use) split del: split_if_asm)
    12.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Mon Jun 16 17:56:08 2008 +0200
    12.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Mon Jun 16 22:13:39 2008 +0200
    12.3 @@ -50,7 +50,7 @@
    12.4  
    12.5  fun deriv_tac ctxt = SUBGOAL (fn (prem, i) =>
    12.6    resolve_tac @{thms deriv_rulesI} i ORELSE
    12.7 -    ((rtac (RuleInsts.read_instantiate ctxt [(("f", 0), get_fun_name prem)]
    12.8 +    ((rtac (read_instantiate ctxt [(("f", 0), get_fun_name prem)]
    12.9                       @{thm DERIV_chain2}) i) handle DERIV_name => no_tac));
   12.10  
   12.11  fun DERIV_tac ctxt = ALLGOALS (fn i => REPEAT (deriv_tac ctxt i));
    13.1 --- a/src/HOL/IMPP/Hoare.thy	Mon Jun 16 17:56:08 2008 +0200
    13.2 +++ b/src/HOL/IMPP/Hoare.thy	Mon Jun 16 22:13:39 2008 +0200
    13.3 @@ -283,7 +283,7 @@
    13.4  apply         (blast) (* cut *)
    13.5  apply        (blast) (* weaken *)
    13.6  apply       (tactic {* ALLGOALS (EVERY'
    13.7 -  [REPEAT o RuleInsts.thin_tac @{context} "hoare_derivs ?x ?y",
    13.8 +  [REPEAT o thin_tac @{context} "hoare_derivs ?x ?y",
    13.9     simp_tac @{simpset}, clarify_tac @{claset}, REPEAT o smp_tac 1]) *})
   13.10  apply       (simp_all (no_asm_use) add: triple_valid_def2)
   13.11  apply       (intro strip, tactic "smp_tac 2 1", blast) (* conseq *)
    14.1 --- a/src/HOL/NanoJava/Equivalence.thy	Mon Jun 16 17:56:08 2008 +0200
    14.2 +++ b/src/HOL/NanoJava/Equivalence.thy	Mon Jun 16 22:13:39 2008 +0200
    14.3 @@ -108,8 +108,8 @@
    14.4  apply (rule hoare_ehoare.induct)
    14.5  (*18*)
    14.6  apply (tactic {* ALLGOALS (REPEAT o dresolve_tac [@{thm all_conjunct2}, @{thm all3_conjunct2}]) *})
    14.7 -apply (tactic {* ALLGOALS (REPEAT o RuleInsts.thin_tac @{context} "hoare ?x ?y") *})
    14.8 -apply (tactic {* ALLGOALS (REPEAT o RuleInsts.thin_tac @{context} "ehoare ?x ?y") *})
    14.9 +apply (tactic {* ALLGOALS (REPEAT o thin_tac @{context} "hoare ?x ?y") *})
   14.10 +apply (tactic {* ALLGOALS (REPEAT o thin_tac @{context} "ehoare ?x ?y") *})
   14.11  apply (simp_all only: cnvalid1_eq cenvalid_def2)
   14.12                   apply fast
   14.13                  apply fast
    15.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Mon Jun 16 17:56:08 2008 +0200
    15.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Mon Jun 16 22:13:39 2008 +0200
    15.3 @@ -54,7 +54,7 @@
    15.4    gen_res_inst_tac_term (K Drule.cterm_instantiate) [];
    15.5  
    15.6  fun cut_inst_tac_term' tinst th =
    15.7 -  res_inst_tac_term' tinst false (Tactic.make_elim_preserve th);
    15.8 +  res_inst_tac_term' tinst false (RuleInsts.make_elim_preserve th);
    15.9  
   15.10  fun get_dyn_thm thy name atom_name =
   15.11    PureThy.get_thm thy name handle ERROR _ =>
    16.1 --- a/src/HOL/Prolog/prolog.ML	Mon Jun 16 17:56:08 2008 +0200
    16.2 +++ b/src/HOL/Prolog/prolog.ML	Mon Jun 16 22:13:39 2008 +0200
    16.3 @@ -53,7 +53,7 @@
    16.4  fun atomizeD ctxt thm = let
    16.5      fun at  thm = case concl_of thm of
    16.6        _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS
    16.7 -        (RuleInsts.read_instantiate ctxt [(("x", 0), "?" ^ (if s="P" then "PP" else s))] spec))
    16.8 +        (read_instantiate ctxt [(("x", 0), "?" ^ (if s="P" then "PP" else s))] spec))
    16.9      | _$(Const("op &",_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
   16.10      | _$(Const("op -->",_)$_$_)     => at(thm RS mp)
   16.11      | _                             => [thm]
    17.1 --- a/src/HOL/Real/rat_arith.ML	Mon Jun 16 17:56:08 2008 +0200
    17.2 +++ b/src/HOL/Real/rat_arith.ML	Mon Jun 16 22:13:39 2008 +0200
    17.3 @@ -14,7 +14,7 @@
    17.4  
    17.5  val simps =
    17.6   [@{thm order_less_irrefl}, @{thm neg_less_iff_less}, @{thm True_implies_equals},
    17.7 -  RuleInsts.read_instantiate @{context} [(("a", 0), "(number_of ?v)")] @{thm right_distrib},
    17.8 +  read_instantiate @{context} [(("a", 0), "(number_of ?v)")] @{thm right_distrib},
    17.9    @{thm divide_1}, @{thm divide_zero_left},
   17.10    @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
   17.11    @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
    18.1 --- a/src/HOL/SET-Protocol/MessageSET.thy	Mon Jun 16 17:56:08 2008 +0200
    18.2 +++ b/src/HOL/SET-Protocol/MessageSET.thy	Mon Jun 16 22:13:39 2008 +0200
    18.3 @@ -880,7 +880,7 @@
    18.4       (EVERY
    18.5        [  (*push in occurrences of X...*)
    18.6         (REPEAT o CHANGED)
    18.7 -           (RuleInsts.res_inst_tac (Simplifier.the_context ss)
    18.8 +           (res_inst_tac (Simplifier.the_context ss)
    18.9               [(("x", 1), "X")] (insert_commute RS ssubst) 1),
   18.10         (*...allowing further simplifications*)
   18.11         simp_tac ss 1,
    19.1 --- a/src/HOL/TLA/TLA.thy	Mon Jun 16 17:56:08 2008 +0200
    19.2 +++ b/src/HOL/TLA/TLA.thy	Mon Jun 16 22:13:39 2008 +0200
    19.3 @@ -307,15 +307,15 @@
    19.4  
    19.5  fun merge_temp_box_tac ctxt i =
    19.6     REPEAT_DETERM (EVERY [etac @{thm box_conjE_temp} i, atac i,
    19.7 -                         RuleInsts.eres_inst_tac ctxt [(("'a", 0), "behavior")] @{thm box_thin} i])
    19.8 +                         eres_inst_tac ctxt [(("'a", 0), "behavior")] @{thm box_thin} i])
    19.9  
   19.10  fun merge_stp_box_tac ctxt i =
   19.11     REPEAT_DETERM (EVERY [etac @{thm box_conjE_stp} i, atac i,
   19.12 -                         RuleInsts.eres_inst_tac ctxt [(("'a", 0), "state")] @{thm box_thin} i])
   19.13 +                         eres_inst_tac ctxt [(("'a", 0), "state")] @{thm box_thin} i])
   19.14  
   19.15  fun merge_act_box_tac ctxt i =
   19.16     REPEAT_DETERM (EVERY [etac @{thm box_conjE_act} i, atac i,
   19.17 -                         RuleInsts.eres_inst_tac ctxt [(("'a", 0), "state * state")] @{thm box_thin} i])
   19.18 +                         eres_inst_tac ctxt [(("'a", 0), "state * state")] @{thm box_thin} i])
   19.19  *}
   19.20  
   19.21  (* rewrite rule to push universal quantification through box:
    20.1 --- a/src/HOL/Tools/TFL/post.ML	Mon Jun 16 17:56:08 2008 +0200
    20.2 +++ b/src/HOL/Tools/TFL/post.ML	Mon Jun 16 22:13:39 2008 +0200
    20.3 @@ -152,7 +152,7 @@
    20.4    rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE)));
    20.5  
    20.6  (*Strip off the outer !P*)
    20.7 -val spec'= RuleInsts.read_instantiate @{context} [(("x", 0), "P::?'b=>bool")] spec;
    20.8 +val spec'= read_instantiate @{context} [(("x", 0), "P::?'b=>bool")] spec;
    20.9  
   20.10  fun tracing true _ = ()
   20.11    | tracing false msg = writeln msg;
    21.1 --- a/src/HOL/Tools/induct_tacs.ML	Mon Jun 16 17:56:08 2008 +0200
    21.2 +++ b/src/HOL/Tools/induct_tacs.ML	Mon Jun 16 22:13:39 2008 +0200
    21.3 @@ -44,7 +44,7 @@
    21.4        (case Induct.vars_of (Thm.term_of (Thm.cprem_of rule 1)) of
    21.5          Var (xi, _) :: _ => xi
    21.6        | _ => raise THM ("Malformed cases rule", 0, [rule]));
    21.7 -  in RuleInsts.res_inst_tac ctxt [(xi, s)] rule i st end
    21.8 +  in res_inst_tac ctxt [(xi, s)] rule i st end
    21.9    handle THM _ => Seq.empty;
   21.10  
   21.11  fun case_tac ctxt s = gen_case_tac ctxt (s, NONE);
   21.12 @@ -100,7 +100,7 @@
   21.13      val concls = HOLogic.dest_concls (Thm.concl_of rule);
   21.14      val insts = maps prep_inst (concls ~~ varss) handle Library.UnequalLengths =>
   21.15        error "Induction rule has different numbers of variables";
   21.16 -  in RuleInsts.res_inst_tac ctxt insts rule i st end
   21.17 +  in res_inst_tac ctxt insts rule i st end
   21.18    handle THM _ => Seq.empty;
   21.19  
   21.20  end;
    22.1 --- a/src/HOL/Tools/meson.ML	Mon Jun 16 17:56:08 2008 +0200
    22.2 +++ b/src/HOL/Tools/meson.ML	Mon Jun 16 22:13:39 2008 +0200
    22.3 @@ -646,7 +646,7 @@
    22.4  (*Rules to convert the head literal into a negated assumption. If the head
    22.5    literal is already negated, then using notEfalse instead of notEfalse'
    22.6    prevents a double negation.*)
    22.7 -val notEfalse = RuleInsts.read_instantiate @{context} [(("R", 0), "False")] notE;
    22.8 +val notEfalse = read_instantiate @{context} [(("R", 0), "False")] notE;
    22.9  val notEfalse' = rotate_prems 1 notEfalse;
   22.10  
   22.11  fun negated_asm_of_head th =
    23.1 --- a/src/HOL/Tools/metis_tools.ML	Mon Jun 16 17:56:08 2008 +0200
    23.2 +++ b/src/HOL/Tools/metis_tools.ML	Mon Jun 16 22:13:39 2008 +0200
    23.3 @@ -24,10 +24,10 @@
    23.4    (* ------------------------------------------------------------------------- *)
    23.5    (* Useful Theorems                                                           *)
    23.6    (* ------------------------------------------------------------------------- *)
    23.7 -  val EXCLUDED_MIDDLE = rotate_prems 1 (RuleInsts.read_instantiate @{context} [(("R", 0), "False")] notE);
    23.8 +  val EXCLUDED_MIDDLE = rotate_prems 1 (read_instantiate @{context} [(("R", 0), "False")] notE);
    23.9    val REFL_THM = incr_indexes 2 (Meson.make_meta_clause refl);  (*Rename from 0,1*)
   23.10    val subst_em  = zero_var_indexes (subst RS EXCLUDED_MIDDLE);
   23.11 -  val ssubst_em = RuleInsts.read_instantiate @{context} [(("t", 0), "?s"), (("s", 0), "?t")] (sym RS subst_em);
   23.12 +  val ssubst_em = read_instantiate @{context} [(("t", 0), "?s"), (("s", 0), "?t")] (sym RS subst_em);
   23.13  
   23.14    (* ------------------------------------------------------------------------- *)
   23.15    (* Useful Functions                                                          *)
    24.1 --- a/src/HOL/Tools/record_package.ML	Mon Jun 16 17:56:08 2008 +0200
    24.2 +++ b/src/HOL/Tools/record_package.ML	Mon Jun 16 22:13:39 2008 +0200
    24.3 @@ -2155,8 +2155,8 @@
    24.4  
    24.5     fun equality_prf () = prove_standard [] equality_prop (fn {context, ...} =>
    24.6        fn st => let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in
    24.7 -        st |> (RuleInsts.res_inst_tac context [((rN, 0), s)] cases_scheme 1
    24.8 -        THEN RuleInsts.res_inst_tac context [((rN, 0), s')] cases_scheme 1
    24.9 +        st |> (res_inst_tac context [((rN, 0), s)] cases_scheme 1
   24.10 +        THEN res_inst_tac context [((rN, 0), s')] cases_scheme 1
   24.11          THEN (METAHYPS equality_tac 1))
   24.12               (* simp_all_tac ss (sel_convs) would also work but is less efficient *)
   24.13        end);
    25.1 --- a/src/HOL/Tools/split_rule.ML	Mon Jun 16 17:56:08 2008 +0200
    25.2 +++ b/src/HOL/Tools/split_rule.ML	Mon Jun 16 22:13:39 2008 +0200
    25.3 @@ -124,7 +124,7 @@
    25.4  
    25.5  
    25.6  fun pair_tac ctxt s =
    25.7 -  RuleInsts.res_inst_tac ctxt [(("p", 0), s)] @{thm PairE}
    25.8 +  res_inst_tac ctxt [(("p", 0), s)] @{thm PairE}
    25.9    THEN' hyp_subst_tac
   25.10    THEN' K prune_params_tac;
   25.11  
    26.1 --- a/src/HOL/UNITY/UNITY_tactics.ML	Mon Jun 16 17:56:08 2008 +0200
    26.2 +++ b/src/HOL/UNITY/UNITY_tactics.ML	Mon Jun 16 22:13:39 2008 +0200
    26.3 @@ -41,9 +41,9 @@
    26.4                                      @{thm EnsuresI}, @{thm ensuresI}] 1),
    26.5                (*now there are two subgoals: co & transient*)
    26.6                simp_tac (ss addsimps [@{thm mk_total_program_def}]) 2,
    26.7 -              RuleInsts.res_inst_tac (Simplifier.the_context ss)
    26.8 +              res_inst_tac (Simplifier.the_context ss)
    26.9                  [(("act", 0), sact)] @{thm totalize_transientI} 2
   26.10 -              ORELSE RuleInsts.res_inst_tac (Simplifier.the_context ss)
   26.11 +              ORELSE res_inst_tac (Simplifier.the_context ss)
   26.12                  [(("act", 0), sact)] @{thm transientI} 2,
   26.13                   (*simplify the command's domain*)
   26.14                simp_tac (ss addsimps [@{thm Domain_def}]) 3,
    27.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Mon Jun 16 17:56:08 2008 +0200
    27.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Mon Jun 16 22:13:39 2008 +0200
    27.3 @@ -1089,7 +1089,7 @@
    27.4  ML {*
    27.5  
    27.6  fun Seq_case_tac ctxt s i =
    27.7 -  RuleInsts.res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_cases} i
    27.8 +  res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_cases} i
    27.9    THEN hyp_subst_tac i THEN hyp_subst_tac (i+1) THEN hyp_subst_tac (i+2);
   27.10  
   27.11  (* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *)
   27.12 @@ -1104,7 +1104,7 @@
   27.13  (* rws are definitions to be unfolded for admissibility check *)
   27.14  fun Seq_induct_tac ctxt s rws i =
   27.15    let val ss = Simplifier.local_simpset_of ctxt in
   27.16 -    RuleInsts.res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i
   27.17 +    res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i
   27.18      THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ss (i+1))))
   27.19      THEN simp_tac (ss addsimps rws) i
   27.20    end;
   27.21 @@ -1114,13 +1114,13 @@
   27.22    THEN (REPEAT_DETERM (CHANGED (asm_simp_tac (Simplifier.local_simpset_of ctxt) i)));
   27.23  
   27.24  fun pair_tac ctxt s =
   27.25 -  RuleInsts.res_inst_tac ctxt [(("p", 0), s)] PairE
   27.26 +  res_inst_tac ctxt [(("p", 0), s)] PairE
   27.27    THEN' hyp_subst_tac THEN' asm_full_simp_tac (Simplifier.local_simpset_of ctxt);
   27.28  
   27.29  (* induction on a sequence of pairs with pairsplitting and simplification *)
   27.30  fun pair_induct_tac ctxt s rws i =
   27.31    let val ss = Simplifier.local_simpset_of ctxt in
   27.32 -    RuleInsts.res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i
   27.33 +    res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i
   27.34      THEN pair_tac ctxt "a" (i+3)
   27.35      THEN (REPEAT_DETERM (CHANGED (simp_tac ss (i+1))))
   27.36      THEN simp_tac (ss addsimps rws) i
    28.1 --- a/src/HOLCF/Tools/domain/domain_library.ML	Mon Jun 16 17:56:08 2008 +0200
    28.2 +++ b/src/HOLCF/Tools/domain/domain_library.ML	Mon Jun 16 22:13:39 2008 +0200
    28.3 @@ -24,7 +24,7 @@
    28.4  fun upd_second f (x,y,z) = (  x, f y,   z);
    28.5  fun upd_third  f (x,y,z) = (  x,   y, f z);
    28.6  
    28.7 -fun atomize ctxt thm = let val r_inst = RuleInsts.read_instantiate ctxt;
    28.8 +fun atomize ctxt thm = let val r_inst = read_instantiate ctxt;
    28.9      fun at  thm = case concl_of thm of
   28.10        _$(Const("op &",_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
   28.11      | _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec))
    29.1 --- a/src/HOLCF/Tools/domain/domain_theorems.ML	Mon Jun 16 17:56:08 2008 +0200
    29.2 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Mon Jun 16 22:13:39 2008 +0200
    29.3 @@ -376,7 +376,7 @@
    29.4        val goal = lift_defined %: (nonlazy args, concl);
    29.5        fun tacs ctxt = [
    29.6          rtac @{thm rev_contrapos} 1,
    29.7 -        RuleInsts.eres_inst_tac ctxt [(("f", 0), dis_name con)] cfun_arg_cong 1,
    29.8 +        eres_inst_tac ctxt [(("f", 0), dis_name con)] cfun_arg_cong 1,
    29.9          asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
   29.10      in pg [] goal tacs end;
   29.11  in
   29.12 @@ -477,7 +477,7 @@
   29.13                          mk_trp (con_app con1 args1 ~<< con_app con2 args2));
   29.14          fun tacs ctxt = [
   29.15            rtac @{thm rev_contrapos} 1,
   29.16 -          RuleInsts.eres_inst_tac ctxt [(("f", 0), dis_name con1)] monofun_cfun_arg 1]
   29.17 +          eres_inst_tac ctxt [(("f", 0), dis_name con1)] monofun_cfun_arg 1]
   29.18            @ map (case_UU_tac ctxt (con_stricts @ dis_rews) 1) (nonlazy args2)
   29.19            @ [asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
   29.20        in pg [] goal tacs end;
   29.21 @@ -709,7 +709,7 @@
   29.22       mk_trp (foldr1 mk_conj (mapn concf 1 dnames)));
   29.23    val take_ss = HOL_ss addsimps take_rews;
   29.24    fun quant_tac ctxt i = EVERY
   29.25 -    (mapn (fn n => fn _ => RuleInsts.res_inst_tac ctxt [(("x", 0), x_name n)] spec i) 1 dnames);
   29.26 +    (mapn (fn n => fn _ => res_inst_tac ctxt [(("x", 0), x_name n)] spec i) 1 dnames);
   29.27  
   29.28    fun ind_prems_tac prems = EVERY
   29.29      (maps (fn cons =>
   29.30 @@ -766,7 +766,7 @@
   29.31              map (K (atac 1))      (nonlazy args) @
   29.32              map (K (etac spec 1)) (List.filter is_rec args);
   29.33            fun cases_tacs (cons, cases) =
   29.34 -            RuleInsts.res_inst_tac context [(("x", 0), "x")] cases 1 ::
   29.35 +            res_inst_tac context [(("x", 0), "x")] cases 1 ::
   29.36              asm_simp_tac (take_ss addsimps prems) 1 ::
   29.37              maps con_tacs cons;
   29.38          in
   29.39 @@ -783,8 +783,8 @@
   29.40            val concl = mk_trp (%:(x_name n) === %:(x_name n^"'"));
   29.41            val goal = mk_All ("n", mk_trp (lhs === rhs)) ===> concl;
   29.42            fun tacf {prems, context} = [
   29.43 -            RuleInsts.res_inst_tac context [(("t", 0), x_name n    )] (ax_reach RS subst) 1,
   29.44 -            RuleInsts.res_inst_tac context [(("t", 0), x_name n^"'")] (ax_reach RS subst) 1,
   29.45 +            res_inst_tac context [(("t", 0), x_name n    )] (ax_reach RS subst) 1,
   29.46 +            res_inst_tac context [(("t", 0), x_name n^"'")] (ax_reach RS subst) 1,
   29.47              stac fix_def2 1,
   29.48              REPEAT (CHANGED
   29.49                (rtac (contlub_cfun_arg RS ssubst) 1 THEN chain_tac 1)),
   29.50 @@ -833,7 +833,7 @@
   29.51              val goal =
   29.52                mk_trp (mk_all ("n", foldr1 mk_conj (mapn mk_eqn 1 eqs)));
   29.53              fun arg_tacs ctxt vn = [
   29.54 -              RuleInsts.eres_inst_tac ctxt [(("x", 0), vn)] all_dupE 1,
   29.55 +              eres_inst_tac ctxt [(("x", 0), vn)] all_dupE 1,
   29.56                etac disjE 1,
   29.57                asm_simp_tac (HOL_ss addsimps con_rews) 1,
   29.58                asm_simp_tac take_ss 1];
   29.59 @@ -843,7 +843,7 @@
   29.60              fun foo_tacs ctxt n (cons, cases) =
   29.61                simp_tac take_ss 1 ::
   29.62                rtac allI 1 ::
   29.63 -              RuleInsts.res_inst_tac ctxt [(("x", 0), x_name n)] cases 1 ::
   29.64 +              res_inst_tac ctxt [(("x", 0), x_name n)] cases 1 ::
   29.65                asm_simp_tac take_ss 1 ::
   29.66                maps (con_tacs ctxt) cons;
   29.67              fun tacs ctxt =
   29.68 @@ -887,8 +887,7 @@
   29.69      else (* infinite case *)
   29.70        let
   29.71          fun one_finite n dn =
   29.72 -          RuleInsts.read_instantiate global_ctxt
   29.73 -            [(("P", 0), dn ^ "_finite " ^ x_name n)] excluded_middle;
   29.74 +          read_instantiate global_ctxt [(("P", 0), dn ^ "_finite " ^ x_name n)] excluded_middle;
   29.75          val finites = mapn one_finite 1 dnames;
   29.76  
   29.77          val goal =
   29.78 @@ -936,7 +935,7 @@
   29.79        fun x_tacs ctxt n x = [
   29.80          rotate_tac (n+1) 1,
   29.81          etac all2E 1,
   29.82 -        RuleInsts.eres_inst_tac ctxt [(("P", 1), sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1,
   29.83 +        eres_inst_tac ctxt [(("P", 1), sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1,
   29.84          TRY (safe_tac HOL_cs),
   29.85          REPEAT (CHANGED (asm_simp_tac take_ss 1))];
   29.86        fun tacs ctxt = [
    30.1 --- a/src/LCF/LCF.thy	Mon Jun 16 17:56:08 2008 +0200
    30.2 +++ b/src/LCF/LCF.thy	Mon Jun 16 22:13:39 2008 +0200
    30.3 @@ -317,7 +317,7 @@
    30.4  
    30.5  ML {*
    30.6    fun induct_tac ctxt v i =
    30.7 -    RuleInsts.res_inst_tac ctxt [(("f", 0), v)] @{thm induct} i THEN
    30.8 +    res_inst_tac ctxt [(("f", 0), v)] @{thm induct} i THEN
    30.9      REPEAT (resolve_tac @{thms adm_lemmas} i)
   30.10  *}
   30.11  
   30.12 @@ -376,7 +376,7 @@
   30.13  
   30.14  ML {*
   30.15  fun induct2_tac ctxt (f, g) i =
   30.16 -  RuleInsts.res_inst_tac ctxt [(("f", 0), f), (("g", 0), g)] @{thm induct2} i THEN
   30.17 +  res_inst_tac ctxt [(("f", 0), f), (("g", 0), g)] @{thm induct2} i THEN
   30.18    REPEAT(resolve_tac @{thms adm_lemmas} i)
   30.19  *}
   30.20  
    31.1 --- a/src/Sequents/LK0.thy	Mon Jun 16 17:56:08 2008 +0200
    31.2 +++ b/src/Sequents/LK0.thy	Mon Jun 16 22:13:39 2008 +0200
    31.3 @@ -157,11 +157,11 @@
    31.4  ML {*
    31.5  (*Cut and thin, replacing the right-side formula*)
    31.6  fun cutR_tac ctxt s i =
    31.7 -  RuleInsts.res_inst_tac ctxt [(("P", 0), s) ] @{thm cut} i  THEN  rtac @{thm thinR} i
    31.8 +  res_inst_tac ctxt [(("P", 0), s) ] @{thm cut} i  THEN  rtac @{thm thinR} i
    31.9  
   31.10  (*Cut and thin, replacing the left-side formula*)
   31.11  fun cutL_tac ctxt s i =
   31.12 -  RuleInsts.res_inst_tac ctxt [(("P", 0), s)] @{thm cut} i  THEN  rtac @{thm thinL} (i+1)
   31.13 +  res_inst_tac ctxt [(("P", 0), s)] @{thm cut} i  THEN  rtac @{thm thinL} (i+1)
   31.14  *}
   31.15  
   31.16  
    32.1 --- a/src/ZF/Tools/induct_tacs.ML	Mon Jun 16 17:56:08 2008 +0200
    32.2 +++ b/src/ZF/Tools/induct_tacs.ML	Mon Jun 16 22:13:39 2008 +0200
    32.3 @@ -102,7 +102,7 @@
    32.4               [] => error "induction is not available for this datatype"
    32.5             | major::_ => FOLogic.dest_Trueprop major)
    32.6    in
    32.7 -    RuleInsts.eres_inst_tac ctxt [(ixn, var)] rule i state
    32.8 +    eres_inst_tac ctxt [(ixn, var)] rule i state
    32.9    end
   32.10    handle Find_tname msg =>
   32.11              if exh then (*try boolean case analysis instead*)
    33.1 --- a/src/ZF/UNITY/SubstAx.thy	Mon Jun 16 17:56:08 2008 +0200
    33.2 +++ b/src/ZF/UNITY/SubstAx.thy	Mon Jun 16 22:13:39 2008 +0200
    33.3 @@ -360,7 +360,7 @@
    33.4                                      @{thm EnsuresI}, @{thm ensuresI}] 1),
    33.5                (*now there are two subgoals: co & transient*)
    33.6                simp_tac (ss addsimps (ProgramDefs.get ctxt)) 2,
    33.7 -              RuleInsts.res_inst_tac ctxt [(("act", 0), sact)] @{thm transientI} 2,
    33.8 +              res_inst_tac ctxt [(("act", 0), sact)] @{thm transientI} 2,
    33.9                   (*simplify the command's domain*)
   33.10                simp_tac (ss addsimps [@{thm domain_def}]) 3, 
   33.11                (* proving the domain part *)
    34.1 --- a/src/ZF/ind_syntax.ML	Mon Jun 16 17:56:08 2008 +0200
    34.2 +++ b/src/ZF/ind_syntax.ML	Mon Jun 16 22:13:39 2008 +0200
    34.3 @@ -51,7 +51,7 @@
    34.4  (*For deriving cases rules.  CollectD2 discards the domain, which is redundant;
    34.5    read_instantiate replaces a propositional variable by a formula variable*)
    34.6  val equals_CollectD =
    34.7 -    RuleInsts.read_instantiate @{context} [(("W", 0), "?Q")]
    34.8 +    read_instantiate @{context} [(("W", 0), "?Q")]
    34.9          (make_elim (@{thm equalityD1} RS @{thm subsetD} RS @{thm CollectD2}));
   34.10  
   34.11