# HG changeset patch # User wenzelm # Date 1213200120 -7200 # Node ID 56b6cdce22f1b6f136002fc764e96d167e4e319e # Parent 192954a9a549d00bdfd47d9d91e742e81cfd3562 Drule.read_instantiate; diff -r 192954a9a549 -r 56b6cdce22f1 src/HOL/Bali/Basis.thy --- 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] *) diff -r 192954a9a549 -r 56b6cdce22f1 src/HOL/Hyperreal/MacLaurin.thy --- 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)); diff -r 192954a9a549 -r 56b6cdce22f1 src/HOL/Nominal/nominal_inductive.ML --- 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); diff -r 192954a9a549 -r 56b6cdce22f1 src/HOL/Nominal/nominal_package.ML --- 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 \ (pi2 \ 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"; diff -r 192954a9a549 -r 56b6cdce22f1 src/HOL/Prolog/prolog.ML --- 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) diff -r 192954a9a549 -r 56b6cdce22f1 src/HOL/Tools/TFL/post.ML --- 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; diff -r 192954a9a549 -r 56b6cdce22f1 src/HOL/Tools/meson.ML --- 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 = diff -r 192954a9a549 -r 56b6cdce22f1 src/HOL/Tools/metis_tools.ML --- 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 *) diff -r 192954a9a549 -r 56b6cdce22f1 src/HOLCF/Tools/domain/domain_library.ML --- 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)) diff -r 192954a9a549 -r 56b6cdce22f1 src/HOLCF/Tools/domain/domain_theorems.ML --- 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; diff -r 192954a9a549 -r 56b6cdce22f1 src/ZF/ind_syntax.ML --- 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}));