--- a/src/HOL/Bali/Basis.thy Wed Jun 11 18:01:36 2008 +0200
+++ b/src/HOL/Bali/Basis.thy Wed Jun 11 18:02:00 2008 +0200
@@ -229,7 +229,7 @@
ML {*
fun sum3_instantiate thm = map (fn s => simplify(simpset()delsimps[@{thm not_None_eq}])
- (read_instantiate [("t","In"^s^" ?x")] thm)) ["1l","2","3","1r"]
+ (Drule.read_instantiate [("t","In"^s^" ?x")] thm)) ["1l","2","3","1r"]
*}
(* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
--- a/src/HOL/Hyperreal/MacLaurin.thy Wed Jun 11 18:01:36 2008 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy Wed Jun 11 18:02:00 2008 +0200
@@ -51,7 +51,7 @@
val deriv_tac =
SUBGOAL (fn (prem,i) =>
(resolve_tac @{thms deriv_rulesI} i) ORELSE
- ((rtac (read_instantiate [("f",get_fun_name prem)]
+ ((rtac (Drule.read_instantiate [("f",get_fun_name prem)]
@{thm DERIV_chain2}) i) handle DERIV_name => no_tac));;
val DERIV_tac = ALLGOALS(fn i => REPEAT(deriv_tac i));
--- a/src/HOL/Nominal/nominal_inductive.ML Wed Jun 11 18:01:36 2008 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Wed Jun 11 18:02:00 2008 +0200
@@ -48,7 +48,7 @@
then SOME perm_bool else NONE
| _ => NONE);
-val allE_Nil = read_instantiate_sg (the_context()) [("x", "[]")] allE;
+val allE_Nil = Drule.read_instantiate_sg (the_context()) [("x", "[]")] allE;
fun transp ([] :: _) = []
| transp xs = map hd xs :: transp (map tl xs);
--- a/src/HOL/Nominal/nominal_package.ML Wed Jun 11 18:01:36 2008 +0200
+++ b/src/HOL/Nominal/nominal_package.ML Wed Jun 11 18:02:00 2008 +0200
@@ -155,7 +155,7 @@
val perm_simproc =
Simplifier.simproc (the_context ()) "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc';
-val allE_Nil = read_instantiate_sg (the_context()) [("x", "[]")] allE;
+val allE_Nil = Drule.read_instantiate_sg (the_context()) [("x", "[]")] allE;
val meta_spec = thm "meta_spec";
--- a/src/HOL/Prolog/prolog.ML Wed Jun 11 18:01:36 2008 +0200
+++ b/src/HOL/Prolog/prolog.ML Wed Jun 11 18:02:00 2008 +0200
@@ -52,7 +52,7 @@
fun atomizeD thm = let
fun at thm = case concl_of thm of
- _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (read_instantiate [("x",
+ _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (Drule.read_instantiate [("x",
"?"^(if s="P" then "PP" else s))] spec))
| _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
| _$(Const("op -->",_)$_$_) => at(thm RS mp)
--- a/src/HOL/Tools/TFL/post.ML Wed Jun 11 18:01:36 2008 +0200
+++ b/src/HOL/Tools/TFL/post.ML Wed Jun 11 18:02:00 2008 +0200
@@ -152,7 +152,7 @@
rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE)));
(*Strip off the outer !P*)
-val spec'= read_instantiate [("x","P::?'b=>bool")] spec;
+val spec'= Drule.read_instantiate [("x","P::?'b=>bool")] spec;
fun tracing true _ = ()
| tracing false msg = writeln msg;
--- a/src/HOL/Tools/meson.ML Wed Jun 11 18:01:36 2008 +0200
+++ b/src/HOL/Tools/meson.ML Wed Jun 11 18:02:00 2008 +0200
@@ -646,7 +646,7 @@
(*Rules to convert the head literal into a negated assumption. If the head
literal is already negated, then using notEfalse instead of notEfalse'
prevents a double negation.*)
-val notEfalse = read_instantiate [("R","False")] notE;
+val notEfalse = Drule.read_instantiate [("R","False")] notE;
val notEfalse' = rotate_prems 1 notEfalse;
fun negated_asm_of_head th =
--- a/src/HOL/Tools/metis_tools.ML Wed Jun 11 18:01:36 2008 +0200
+++ b/src/HOL/Tools/metis_tools.ML Wed Jun 11 18:02:00 2008 +0200
@@ -24,10 +24,10 @@
(* ------------------------------------------------------------------------- *)
(* Useful Theorems *)
(* ------------------------------------------------------------------------- *)
- val EXCLUDED_MIDDLE = rotate_prems 1 (read_instantiate [("R","False")] notE);
+ val EXCLUDED_MIDDLE = rotate_prems 1 (Drule.read_instantiate [("R","False")] notE);
val REFL_THM = incr_indexes 2 (Meson.make_meta_clause refl); (*Rename from 0,1*)
val subst_em = zero_var_indexes (subst RS EXCLUDED_MIDDLE);
- val ssubst_em = read_instantiate [("t","?s"),("s","?t")] (sym RS subst_em);
+ val ssubst_em = Drule.read_instantiate [("t","?s"),("s","?t")] (sym RS subst_em);
(* ------------------------------------------------------------------------- *)
(* Useful Functions *)
--- a/src/HOLCF/Tools/domain/domain_library.ML Wed Jun 11 18:01:36 2008 +0200
+++ b/src/HOLCF/Tools/domain/domain_library.ML Wed Jun 11 18:02:00 2008 +0200
@@ -24,7 +24,7 @@
fun upd_second f (x,y,z) = ( x, f y, z);
fun upd_third f (x,y,z) = ( x, y, f z);
-fun atomize thm = let val r_inst = read_instantiate;
+fun atomize thm = let val r_inst = Drule.read_instantiate;
fun at thm = case concl_of thm of
_$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
| _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (r_inst [("x","?"^s)] spec))
--- a/src/HOLCF/Tools/domain/domain_theorems.ML Wed Jun 11 18:01:36 2008 +0200
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML Wed Jun 11 18:02:00 2008 +0200
@@ -884,7 +884,7 @@
else (* infinite case *)
let
fun one_finite n dn =
- read_instantiate_sg thy
+ Drule.read_instantiate_sg thy
[("P",dn^"_finite "^x_name n)] excluded_middle;
val finites = mapn one_finite 1 dnames;
--- a/src/ZF/ind_syntax.ML Wed Jun 11 18:01:36 2008 +0200
+++ b/src/ZF/ind_syntax.ML Wed Jun 11 18:02:00 2008 +0200
@@ -51,7 +51,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 [("W","?Q")]
+ Drule.read_instantiate [("W","?Q")]
(make_elim (@{thm equalityD1} RS @{thm subsetD} RS @{thm CollectD2}));