# HG changeset patch
# User wenzelm
# Date 877706001 -7200
# Node ID 4cb2f2422695dceb8e29e9ee7dd7db44d0c8824d
# Parent  a8c80f5fdd167e1c18771ec6d4e51da631782c69
ProtoPure.thy;

diff -r a8c80f5fdd16 -r 4cb2f2422695 src/Pure/drule.ML
--- 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
diff -r a8c80f5fdd16 -r 4cb2f2422695 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Fri Oct 24 17:12:35 1997 +0200
+++ b/src/Pure/tactic.ML	Fri Oct 24 17:13:21 1997 +0200
@@ -310,7 +310,7 @@
   increment revcut_rl instead.*)
 fun make_elim_preserve rl = 
   let val {maxidx,...} = rep_thm rl
-      fun cvar ixn = cterm_of Sign.proto_pure (Var(ixn,propT));
+      fun cvar ixn = cterm_of (sign_of ProtoPure.thy) (Var(ixn,propT));
       val revcut_rl' = 
 	  instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
 			     (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
diff -r a8c80f5fdd16 -r 4cb2f2422695 src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Fri Oct 24 17:12:35 1997 +0200
+++ b/src/Pure/tctical.ML	Fri Oct 24 17:13:21 1997 +0200
@@ -334,7 +334,7 @@
 (*SELECT_GOAL optimization: replace the conclusion by a variable X,
   to avoid copying.  Proof states have X==concl as an assuption.*)
 
-val prop_equals = cterm_of Sign.proto_pure 
+val prop_equals = cterm_of (sign_of ProtoPure.thy) 
                     (Const("==", propT-->propT-->propT));
 
 fun mk_prop_equals(t,u) = capply (capply prop_equals t) u;
@@ -343,7 +343,7 @@
   It is paired with a function to undo the transformation.  If ct contains
   Vars then it returns ct==>ct.*)
 fun eq_trivial ct =
-  let val xfree = cterm_of Sign.proto_pure (Free (gensym"EQ_TRIVIAL_", propT))
+  let val xfree = cterm_of (sign_of ProtoPure.thy) (Free (gensym"EQ_TRIVIAL_", propT))
       val ct_eq_x = mk_prop_equals (ct, xfree)
       and refl_ct = reflexive ct
       fun restore th = 
@@ -367,7 +367,7 @@
 
 (* (!!selct. PROP ?V) ==> PROP ?V ;  contains NO TYPE VARIABLES.*)
 val dummy_quant_rl = 
-  read_cterm Sign.proto_pure ("!!selct::prop. PROP V",propT) |>
+  read_cterm (sign_of ProtoPure.thy) ("!!selct::prop. PROP V",propT) |>
   assume |> forall_elim_var 0 |> standard;
 
 (* Prevent the subgoal's assumptions from becoming additional subgoals in the
diff -r a8c80f5fdd16 -r 4cb2f2422695 src/Pure/unify.ML
--- a/src/Pure/unify.ML	Fri Oct 24 17:12:35 1997 +0200
+++ b/src/Pure/unify.ML	Fri Oct 24 17:13:21 1997 +0200
@@ -41,7 +41,7 @@
 and trace_types = ref false	(*announce potential incompleteness
 				  of type unification*)
 
-val sgr = ref(Sign.proto_pure);
+val sgr = ref(Sign.pre_pure);
 
 type binderlist = (string*typ) list;