src/Pure/drule.ML
changeset 3991 4cb2f2422695
parent 3766 8e1794c4e81b
child 4016 90aebb69c04e
--- a/src/Pure/drule.ML	Fri Oct 24 17:12:35 1997 +0200
+++ b/src/Pure/drule.ML	Fri Oct 24 17:13:21 1997 +0200
@@ -68,10 +68,10 @@
   val zero_var_indexes	: thm -> thm
 end;
 
-
 structure Drule : DRULE =
 struct
 
+
 (** some cterm->cterm operations: much faster than calling cterm_of! **)
 
 (** SAME NAMES as in structure Logic: use compound identifiers! **)
@@ -389,22 +389,22 @@
 (*** Meta-Rewriting Rules ***)
 
 val reflexive_thm =
-  let val cx = cterm_of Sign.proto_pure (Var(("x",0),TVar(("'a",0),logicS)))
+  let val cx = cterm_of (sign_of ProtoPure.thy) (Var(("x",0),TVar(("'a",0),logicS)))
   in Thm.reflexive cx end;
 
 val symmetric_thm =
-  let val xy = read_cterm Sign.proto_pure ("x::'a::logic == y",propT)
+  let val xy = read_cterm (sign_of ProtoPure.thy) ("x::'a::logic == y",propT)
   in standard(Thm.implies_intr_hyps(Thm.symmetric(Thm.assume xy))) end;
 
 val transitive_thm =
-  let val xy = read_cterm Sign.proto_pure ("x::'a::logic == y",propT)
-      val yz = read_cterm Sign.proto_pure ("y::'a::logic == z",propT)
+  let val xy = read_cterm (sign_of ProtoPure.thy) ("x::'a::logic == y",propT)
+      val yz = read_cterm (sign_of ProtoPure.thy) ("y::'a::logic == z",propT)
       val xythm = Thm.assume xy and yzthm = Thm.assume yz
   in standard(Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
 
 (** Below, a "conversion" has type cterm -> thm **)
 
-val refl_implies = reflexive (cterm_of Sign.proto_pure implies);
+val refl_implies = reflexive (cterm_of (sign_of ProtoPure.thy) implies);
 
 (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
 (*Do not rewrite flex-flex pairs*)
@@ -474,8 +474,8 @@
     end
     handle THM _ => err th | bind => err th
 in
-val flexpair_intr = flexpair_inst (symmetric flexpair_def)
-and flexpair_elim = flexpair_inst flexpair_def
+val flexpair_intr = flexpair_inst (symmetric ProtoPure.flexpair_def)
+and flexpair_elim = flexpair_inst ProtoPure.flexpair_def
 end;
 
 (*Version for flexflex pairs -- this supports lifting.*)
@@ -486,17 +486,17 @@
 (*** Some useful meta-theorems ***)
 
 (*The rule V/V, obtains assumption solving for eresolve_tac*)
-val asm_rl = trivial(read_cterm Sign.proto_pure ("PROP ?psi",propT));
+val asm_rl = trivial(read_cterm (sign_of ProtoPure.thy) ("PROP ?psi",propT));
 
 (*Meta-level cut rule: [| V==>W; V |] ==> W *)
-val cut_rl = trivial(read_cterm Sign.proto_pure
+val cut_rl = trivial(read_cterm (sign_of ProtoPure.thy)
         ("PROP ?psi ==> PROP ?theta", propT));
 
 (*Generalized elim rule for one conclusion; cut_rl with reversed premises:
      [| PROP V;  PROP V ==> PROP W |] ==> PROP W *)
 val revcut_rl =
-  let val V = read_cterm Sign.proto_pure ("PROP V", propT)
-      and VW = read_cterm Sign.proto_pure ("PROP V ==> PROP W", propT);
+  let val V = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT)
+      and VW = read_cterm (sign_of ProtoPure.thy) ("PROP V ==> PROP W", propT);
   in  standard (implies_intr V
                 (implies_intr VW
                  (implies_elim (assume VW) (assume V))))
@@ -504,16 +504,16 @@
 
 (*for deleting an unwanted assumption*)
 val thin_rl =
-  let val V = read_cterm Sign.proto_pure ("PROP V", propT)
-      and W = read_cterm Sign.proto_pure ("PROP W", propT);
+  let val V = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT)
+      and W = read_cterm (sign_of ProtoPure.thy) ("PROP W", propT);
   in  standard (implies_intr V (implies_intr W (assume W)))
   end;
 
 (* (!!x. PROP ?V) == PROP ?V       Allows removal of redundant parameters*)
 val triv_forall_equality =
-  let val V  = read_cterm Sign.proto_pure ("PROP V", propT)
-      and QV = read_cterm Sign.proto_pure ("!!x::'a. PROP V", propT)
-      and x  = read_cterm Sign.proto_pure ("x", TFree("'a",logicS));
+  let val V  = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT)
+      and QV = read_cterm (sign_of ProtoPure.thy) ("!!x::'a. PROP V", propT)
+      and x  = read_cterm (sign_of ProtoPure.thy) ("x", TFree("'a",logicS));
   in  standard (equal_intr (implies_intr QV (forall_elim x (assume QV)))
                            (implies_intr V  (forall_intr x (assume V))))
   end;
@@ -523,12 +523,12 @@
    `thm COMP swap_prems_rl' swaps the first two premises of `thm'
 *)
 val swap_prems_rl =
-  let val cmajor = read_cterm Sign.proto_pure
+  let val cmajor = read_cterm (sign_of ProtoPure.thy)
             ("PROP PhiA ==> PROP PhiB ==> PROP Psi", propT);
       val major = assume cmajor;
-      val cminor1 = read_cterm Sign.proto_pure  ("PROP PhiA", propT);
+      val cminor1 = read_cterm (sign_of ProtoPure.thy)  ("PROP PhiA", propT);
       val minor1 = assume cminor1;
-      val cminor2 = read_cterm Sign.proto_pure  ("PROP PhiB", propT);
+      val cminor2 = read_cterm (sign_of ProtoPure.thy)  ("PROP PhiB", propT);
       val minor2 = assume cminor2;
   in standard
        (implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1
@@ -540,8 +540,8 @@
    Introduction rule for == using ==> not meta-hyps.
 *)
 val equal_intr_rule =
-  let val PQ = read_cterm Sign.proto_pure ("PROP phi ==> PROP psi", propT)
-      and QP = read_cterm Sign.proto_pure ("PROP psi ==> PROP phi", propT)
+  let val PQ = read_cterm (sign_of ProtoPure.thy) ("PROP phi ==> PROP psi", propT)
+      and QP = read_cterm (sign_of ProtoPure.thy) ("PROP psi ==> PROP phi", propT)
   in  equal_intr (assume PQ) (assume QP)
       |> implies_intr QP
       |> implies_intr PQ