# HG changeset patch
# User wenzelm
# Date 1390740340 -3600
# Node ID f331472f102753d83de11d42366745850588fd35
# Parent  0940309ed8f1a71647f428e10d4afde4734df725
tuned signature;

diff -r 0940309ed8f1 -r f331472f1027 src/HOL/Bali/AxExample.thy
--- 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'
diff -r 0940309ed8f1 -r f331472f1027 src/HOL/Bali/Basis.thy
--- 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] *)
 
diff -r 0940309ed8f1 -r f331472f1027 src/HOL/Prolog/prolog.ML
--- 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]
diff -r 0940309ed8f1 -r f331472f1027 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- 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) =
diff -r 0940309ed8f1 -r f331472f1027 src/HOL/Tools/TFL/post.ML
--- 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;
diff -r 0940309ed8f1 -r f331472f1027 src/Pure/Tools/rule_insts.ML
--- 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
diff -r 0940309ed8f1 -r f331472f1027 src/ZF/ind_syntax.ML
--- 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}));