--- a/src/HOL/Bali/AxExample.thy Sat Jan 25 23:50:49 2014 +0100
+++ b/src/HOL/Bali/AxExample.thy Sun Jan 26 13:45:40 2014 +0100
@@ -42,8 +42,9 @@
ML {*
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)] xs st | NONE => Seq.empty;
+ (case AList.lookup (op =) (rev (Term.add_var_names (Thm.prop_of st) [])) s of
+ SOME i => Rule_Insts.instantiate_tac ctxt [((s, i), t)] xs st
+ | NONE => Seq.empty);
val ax_tac =
REPEAT o rtac allI THEN'
--- a/src/HOL/Bali/Basis.thy Sat Jan 25 23:50:49 2014 +0100
+++ b/src/HOL/Bali/Basis.thy Sun Jan 26 13:45:40 2014 +0100
@@ -179,9 +179,11 @@
where "the_In1r \<equiv> the_Inr \<circ> the_In1"
ML {*
-fun sum3_instantiate ctxt thm = map (fn s =>
- simplify (ctxt delsimps [@{thm not_None_eq}])
- (read_instantiate ctxt [(("t", 0), "In" ^ s ^ " x")] ["x"] thm)) ["1l","2","3","1r"]
+fun sum3_instantiate ctxt thm =
+ map (fn s =>
+ simplify (ctxt delsimps @{thms not_None_eq})
+ (Rule_Insts.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] *)
--- a/src/HOL/Prolog/prolog.ML Sat Jan 25 23:50:49 2014 +0100
+++ b/src/HOL/Prolog/prolog.ML Sun Jan 26 13:45:40 2014 +0100
@@ -54,7 +54,7 @@
fun at thm = case concl_of thm of
_$(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
+ in at(thm RS (Rule_Insts.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]
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sat Jan 25 23:50:49 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sun Jan 26 13:45:40 2014 +0100
@@ -416,7 +416,7 @@
|> 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 |> Rule_Insts.read_instantiate ctxt [((p_name, 0), p_inst)] [])
end
fun type_match thy (T1, T2) =
--- a/src/HOL/Tools/TFL/post.ML Sat Jan 25 23:50:49 2014 +0100
+++ b/src/HOL/Tools/TFL/post.ML Sun Jan 26 13:45:40 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'= Rule_Insts.read_instantiate @{context} [(("x", 0), "P::'b=>bool")] [] spec;
fun tracing true _ = ()
| tracing false msg = writeln msg;
--- a/src/Pure/Tools/rule_insts.ML Sat Jan 25 23:50:49 2014 +0100
+++ b/src/Pure/Tools/rule_insts.ML Sun Jan 26 13:45:40 2014 +0100
@@ -6,8 +6,6 @@
signature BASIC_RULE_INSTS =
sig
- 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
@@ -24,6 +22,8 @@
(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 read_instantiate: Proof.context -> (indexname * string) list -> string list -> thm -> thm
+ val instantiate_tac: Proof.context -> (indexname * string) list -> string list -> tactic
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
--- a/src/ZF/ind_syntax.ML Sat Jan 25 23:50:49 2014 +0100
+++ b/src/ZF/ind_syntax.ML Sun Jan 26 13:45:40 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")] ["Q"]
+ Rule_Insts.read_instantiate @{context} [(("W", 0), "Q")] ["Q"]
(make_elim (@{thm equalityD1} RS @{thm subsetD} RS @{thm CollectD2}));