RuleInsts.read_instantiate;
authorwenzelm
Mon Jun 16 17:54:43 2008 +0200 (2008-06-16)
changeset 27230c0103bc7f7eb
parent 27229 f656a12e0f4e
child 27231 ef7cc91a0d7f
RuleInsts.read_instantiate;
src/HOL/Tools/TFL/post.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/metis_tools.ML
src/ZF/ind_syntax.ML
     1.1 --- a/src/HOL/Tools/TFL/post.ML	Mon Jun 16 17:54:42 2008 +0200
     1.2 +++ b/src/HOL/Tools/TFL/post.ML	Mon Jun 16 17:54:43 2008 +0200
     1.3 @@ -152,7 +152,7 @@
     1.4    rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE)));
     1.5  
     1.6  (*Strip off the outer !P*)
     1.7 -val spec'= Drule.read_instantiate [("x","P::?'b=>bool")] spec;
     1.8 +val spec'= RuleInsts.read_instantiate @{context} [(("x", 0), "P::?'b=>bool")] spec;
     1.9  
    1.10  fun tracing true _ = ()
    1.11    | tracing false msg = writeln msg;
     2.1 --- a/src/HOL/Tools/meson.ML	Mon Jun 16 17:54:42 2008 +0200
     2.2 +++ b/src/HOL/Tools/meson.ML	Mon Jun 16 17:54:43 2008 +0200
     2.3 @@ -646,7 +646,7 @@
     2.4  (*Rules to convert the head literal into a negated assumption. If the head
     2.5    literal is already negated, then using notEfalse instead of notEfalse'
     2.6    prevents a double negation.*)
     2.7 -val notEfalse = Drule.read_instantiate [("R","False")] notE;
     2.8 +val notEfalse = RuleInsts.read_instantiate @{context} [(("R", 0), "False")] notE;
     2.9  val notEfalse' = rotate_prems 1 notEfalse;
    2.10  
    2.11  fun negated_asm_of_head th =
     3.1 --- a/src/HOL/Tools/metis_tools.ML	Mon Jun 16 17:54:42 2008 +0200
     3.2 +++ b/src/HOL/Tools/metis_tools.ML	Mon Jun 16 17:54:43 2008 +0200
     3.3 @@ -24,10 +24,10 @@
     3.4    (* ------------------------------------------------------------------------- *)
     3.5    (* Useful Theorems                                                           *)
     3.6    (* ------------------------------------------------------------------------- *)
     3.7 -  val EXCLUDED_MIDDLE  = rotate_prems 1 (Drule.read_instantiate [("R","False")] notE);
     3.8 -  val REFL_THM         = incr_indexes 2 (Meson.make_meta_clause refl);  (*Rename from 0,1*)
     3.9 +  val EXCLUDED_MIDDLE = rotate_prems 1 (RuleInsts.read_instantiate @{context} [(("R", 0), "False")] notE);
    3.10 +  val REFL_THM = incr_indexes 2 (Meson.make_meta_clause refl);  (*Rename from 0,1*)
    3.11    val subst_em  = zero_var_indexes (subst RS EXCLUDED_MIDDLE);
    3.12 -  val ssubst_em  = Drule.read_instantiate [("t","?s"),("s","?t")] (sym RS subst_em);
    3.13 +  val ssubst_em = RuleInsts.read_instantiate @{context} [(("t", 0), "?s"), (("s", 0), "?t")] (sym RS subst_em);
    3.14  
    3.15    (* ------------------------------------------------------------------------- *)
    3.16    (* Useful Functions                                                          *)
     4.1 --- a/src/ZF/ind_syntax.ML	Mon Jun 16 17:54:42 2008 +0200
     4.2 +++ b/src/ZF/ind_syntax.ML	Mon Jun 16 17:54:43 2008 +0200
     4.3 @@ -51,7 +51,7 @@
     4.4  (*For deriving cases rules.  CollectD2 discards the domain, which is redundant;
     4.5    read_instantiate replaces a propositional variable by a formula variable*)
     4.6  val equals_CollectD =
     4.7 -    Drule.read_instantiate [("W","?Q")]
     4.8 +    RuleInsts.read_instantiate @{context} [(("W", 0), "?Q")]
     4.9          (make_elim (@{thm equalityD1} RS @{thm subsetD} RS @{thm CollectD2}));
    4.10  
    4.11