eliminated theory ProtoPure;

--- a/src/HOL/Import/shuffler.ML	Thu Mar 27 14:41:07 2008 +0100
+++ b/src/HOL/Import/shuffler.ML	Thu Mar 27 14:41:09 2008 +0100
@@ -90,7 +90,7 @@
 
 val weaken =
     let
-        val cert = cterm_of ProtoPure.thy
+        val cert = cterm_of Pure.thy
         val P = Free("P",propT)
         val Q = Free("Q",propT)
         val PQ = Logic.mk_implies(P,Q)
@@ -109,7 +109,7 @@
 
 val imp_comm =
     let
-        val cert = cterm_of ProtoPure.thy
+        val cert = cterm_of Pure.thy
         val P = Free("P",propT)
         val Q = Free("Q",propT)
         val R = Free("R",propT)
@@ -129,7 +129,7 @@
 
 val def_norm =
     let
-        val cert = cterm_of ProtoPure.thy
+        val cert = cterm_of Pure.thy
         val aT = TFree("'a",[])
         val bT = TFree("'b",[])
         val v = Free("v",aT)
@@ -156,7 +156,7 @@
 
 val all_comm =
     let
-        val cert = cterm_of ProtoPure.thy
+        val cert = cterm_of Pure.thy
         val xT = TFree("'a",[])
         val yT = TFree("'b",[])
         val P = Free("P",xT-->yT-->propT)
@@ -180,7 +180,7 @@
 
 val equiv_comm =
     let
-        val cert = cterm_of ProtoPure.thy
+        val cert = cterm_of Pure.thy
         val T    = TFree("'a",[])
         val t    = Free("t",T)
         val u    = Free("u",T)

--- a/src/HOL/Tools/ComputeHOL.thy	Thu Mar 27 14:41:07 2008 +0100
+++ b/src/HOL/Tools/ComputeHOL.thy	Thu Mar 27 14:41:09 2008 +0100
@@ -172,12 +172,7 @@
 
 fun prep_thms ths = map (convert_conditions o to_meta_eq) ths
 
-local
-    val sym_HOL = @{thm "HOL.sym"}
-    val sym_Pure = @{thm "ProtoPure.symmetric"}
-in
-  fun symmetric th = ((sym_HOL OF [th]) handle THM _ => (sym_Pure OF [th]))
-end
+fun symmetric th = @{thm "HOL.sym"} OF [th] handle THM _ => @{thm "Pure.symmetric"} OF [th]
 
 local
     val trans_HOL = @{thm "HOL.trans"}

--- a/src/HOL/Tools/meson.ML	Thu Mar 27 14:41:07 2008 +0100
+++ b/src/HOL/Tools/meson.ML	Thu Mar 27 14:41:09 2008 +0100
@@ -291,7 +291,7 @@
 fun resop nf [prem] = resolve_tac (nf prem) 1;
 
 (*Any need to extend this list with
-  "HOL.type_class","HOL.eq_class","ProtoPure.term"?*)
+  "HOL.type_class","HOL.eq_class","Pure.term"?*)
 val has_meta_conn =
     exists_Const (member (op =) ["==", "==>", "all", "prop"] o #1);
 

--- a/src/Pure/Isar/local_defs.ML	Thu Mar 27 14:41:07 2008 +0100
+++ b/src/Pure/Isar/local_defs.ML	Thu Mar 27 14:41:09 2008 +0100
@@ -203,13 +203,11 @@
 
 (* meta rewrite rules *)
 
-val equals_ss =
-  MetaSimplifier.theory_context ProtoPure.thy MetaSimplifier.empty_ss
-    addeqcongs [Drule.equals_cong];    (*protect meta-level equality*)
-
 fun meta_rewrite_conv ctxt =
   MetaSimplifier.rewrite_cterm (false, false, false) (K (K NONE))
-    (equals_ss addsimps (Rules.get (Context.Proof ctxt)));
+    (MetaSimplifier.context ctxt MetaSimplifier.empty_ss
+      addeqcongs [Drule.equals_cong]    (*protect meta-level equality*)
+      addsimps (Rules.get (Context.Proof ctxt)));
 
 val meta_rewrite_rule = Conv.fconv_rule o meta_rewrite_conv;
 

--- a/src/Pure/Proof/proof_rewrite_rules.ML	Thu Mar 27 14:41:07 2008 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Thu Mar 27 14:41:09 2008 +0100
@@ -34,36 +34,36 @@
     val equal_elim_axm = ax equal_elim_axm [];
     val symmetric_axm = ax symmetric_axm [propT];
 
-    fun rew' (PThm ("ProtoPure.protectD", _, _, _) % _ %%
-        (PThm ("ProtoPure.protectI", _, _, _) % _ %% prf)) = SOME prf
-      | rew' (PThm ("ProtoPure.conjunctionD1", _, _, _) % _ % _ %%
-        (PThm ("ProtoPure.conjunctionI", _, _, _) % _ % _ %% prf %% _)) = SOME prf
-      | rew' (PThm ("ProtoPure.conjunctionD2", _, _, _) % _ % _ %%
-        (PThm ("ProtoPure.conjunctionI", _, _, _) % _ % _ %% _ %% prf)) = SOME prf
-      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
-        (PAxm ("ProtoPure.equal_intr", _, _) % _ % _ %% prf %% _)) = SOME prf
-      | rew' (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
-        (PAxm ("ProtoPure.equal_intr", _, _) % A % B %% prf1 %% prf2)) =
+    fun rew' (PThm ("Pure.protectD", _, _, _) % _ %%
+        (PThm ("Pure.protectI", _, _, _) % _ %% prf)) = SOME prf
+      | rew' (PThm ("Pure.conjunctionD1", _, _, _) % _ % _ %%
+        (PThm ("Pure.conjunctionI", _, _, _) % _ % _ %% prf %% _)) = SOME prf
+      | rew' (PThm ("Pure.conjunctionD2", _, _, _) % _ % _ %%
+        (PThm ("Pure.conjunctionI", _, _, _) % _ % _ %% _ %% prf)) = SOME prf
+      | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
+        (PAxm ("Pure.equal_intr", _, _) % _ % _ %% prf %% _)) = SOME prf
+      | rew' (PAxm ("Pure.symmetric", _, _) % _ % _ %%
+        (PAxm ("Pure.equal_intr", _, _) % A % B %% prf1 %% prf2)) =
             SOME (equal_intr_axm % B % A %% prf2 %% prf1)
 
-      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
-        (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("prop", _)) %
-          _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %%
-        ((tg as PThm ("ProtoPure.protectI", _, _, _)) % _ %% prf2)) =
+      | rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
+        (PAxm ("Pure.combination", _, _) % SOME (Const ("prop", _)) %
+          _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %%
+        ((tg as PThm ("Pure.protectI", _, _, _)) % _ %% prf2)) =
         SOME (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
 
-      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
-        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
-          (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("prop", _)) %
-             _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1)) %%
-        ((tg as PThm ("ProtoPure.protectI", _, _, _)) % _ %% prf2)) =
+      | rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
+        (PAxm ("Pure.symmetric", _, _) % _ % _ %%
+          (PAxm ("Pure.combination", _, _) % SOME (Const ("prop", _)) %
+             _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1)) %%
+        ((tg as PThm ("Pure.protectI", _, _, _)) % _ %% prf2)) =
         SOME (tg %> B %% (equal_elim_axm %> A %> B %%
           (symmetric_axm % ?? B % ?? A %% prf1) %% prf2))
 
-      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME X % SOME Y %%
-        (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
-          (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==>", _)) % _ % _ % _ %%
-             (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) =
+      | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
+        (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
+          (PAxm ("Pure.combination", _, _) % SOME (Const ("==>", _)) % _ % _ % _ %%
+             (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2)) =
         let
           val _ $ A $ C = Envir.beta_norm X;
           val _ $ B $ D = Envir.beta_norm Y
@@ -73,11 +73,11 @@
               (symmetric_axm % ?? A % ?? B %% incr_pboundvars 2 0 prf1) %% PBound 0)))))
         end
 
-      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME X % SOME Y %%
-        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
-          (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
-            (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==>", _)) % _ % _ % _ %%
-               (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2))) =
+      | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
+        (PAxm ("Pure.symmetric", _, _) % _ % _ %%
+          (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
+            (PAxm ("Pure.combination", _, _) % SOME (Const ("==>", _)) % _ % _ % _ %%
+               (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2))) =
         let
           val _ $ A $ C = Envir.beta_norm Y;
           val _ $ B $ D = Envir.beta_norm X
@@ -87,10 +87,10 @@
               %% (PBound 1 %% (equal_elim_axm %> A %> B %% incr_pboundvars 2 0 prf1 %% PBound 0)))))
         end
 
-      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME X % SOME Y %%
-        (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("all", _)) % _ % _ % _ %%
-          (PAxm ("ProtoPure.reflexive", _, _) % _) %%
-            (PAxm ("ProtoPure.abstract_rule", _, _) % _ % _ %% prf))) =
+      | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
+        (PAxm ("Pure.combination", _, _) % SOME (Const ("all", _)) % _ % _ % _ %%
+          (PAxm ("Pure.reflexive", _, _) % _) %%
+            (PAxm ("Pure.abstract_rule", _, _) % _ % _ %% prf))) =
         let
           val Const (_, T) $ P = Envir.beta_norm X;
           val _ $ Q = Envir.beta_norm Y;
@@ -99,11 +99,11 @@
               (incr_pboundvars 1 1 prf %> Bound 0) %% (PBound 0 %> Bound 0))))
         end
 
-      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME X % SOME Y %%
-        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%        
-          (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("all", _)) % _ % _ % _ %%
-            (PAxm ("ProtoPure.reflexive", _, _) % _) %%
-              (PAxm ("ProtoPure.abstract_rule", _, _) % _ % _ %% prf)))) =
+      | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
+        (PAxm ("Pure.symmetric", _, _) % _ % _ %%        
+          (PAxm ("Pure.combination", _, _) % SOME (Const ("all", _)) % _ % _ % _ %%
+            (PAxm ("Pure.reflexive", _, _) % _) %%
+              (PAxm ("Pure.abstract_rule", _, _) % _ % _ %% prf)))) =
         let
           val Const (_, T) $ P = Envir.beta_norm X;
           val _ $ Q = Envir.beta_norm Y;
@@ -115,68 +115,68 @@
               %% (PBound 0 %> Bound 0))))
         end
 
-      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME A % SOME C %%
-        (PAxm ("ProtoPure.transitive", _, _) % _ % SOME B % _ %% prf1 %% prf2) %% prf3) =
+      | rew' (PAxm ("Pure.equal_elim", _, _) % SOME A % SOME C %%
+        (PAxm ("Pure.transitive", _, _) % _ % SOME B % _ %% prf1 %% prf2) %% prf3) =
            SOME (equal_elim_axm %> B %> C %% prf2 %%
              (equal_elim_axm %> A %> B %% prf1 %% prf3))
-      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME A % SOME C %%
-        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
-          (PAxm ("ProtoPure.transitive", _, _) % _ % SOME B % _ %% prf1 %% prf2)) %% prf3) =
+      | rew' (PAxm ("Pure.equal_elim", _, _) % SOME A % SOME C %%
+        (PAxm ("Pure.symmetric", _, _) % _ % _ %%
+          (PAxm ("Pure.transitive", _, _) % _ % SOME B % _ %% prf1 %% prf2)) %% prf3) =
            SOME (equal_elim_axm %> B %> C %% (symmetric_axm % ?? C % ?? B %% prf1) %%
              (equal_elim_axm %> A %> B %% (symmetric_axm % ?? B % ?? A %% prf2) %% prf3))
 
-      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
-        (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf) = SOME prf
-      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
-        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
-          (PAxm ("ProtoPure.reflexive", _, _) % _)) %% prf) = SOME prf
+      | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
+        (PAxm ("Pure.reflexive", _, _) % _) %% prf) = SOME prf
+      | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
+        (PAxm ("Pure.symmetric", _, _) % _ % _ %%
+          (PAxm ("Pure.reflexive", _, _) % _)) %% prf) = SOME prf
 
-      | rew' (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
-        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% prf)) = SOME prf
+      | rew' (PAxm ("Pure.symmetric", _, _) % _ % _ %%
+        (PAxm ("Pure.symmetric", _, _) % _ % _ %% prf)) = SOME prf
 
-      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
-        (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %%
-          (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
-            (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
-              (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3) %% prf4) =
+      | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
+        (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %%
+          (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
+            (PAxm ("Pure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
+              (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3) %% prf4) =
           SOME (equal_elim_axm %> C %> D %% prf2 %%
             (equal_elim_axm %> A %> C %% prf3 %%
               (equal_elim_axm %> B %> A %% (symmetric_axm % ?? A % ?? B %% prf1) %% prf4)))
 
-      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
-        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
-          (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %%
-            (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
-              (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
-                (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3)) %% prf4) =
+      | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
+        (PAxm ("Pure.symmetric", _, _) % _ % _ %%
+          (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %%
+            (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
+              (PAxm ("Pure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
+                (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3)) %% prf4) =
           SOME (equal_elim_axm %> A %> B %% prf1 %%
             (equal_elim_axm %> C %> A %% (symmetric_axm % ?? A % ?? C %% prf3) %%
               (equal_elim_axm %> D %> C %% (symmetric_axm % ?? C % ?? D %% prf2) %% prf4)))
 
-      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
-        (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %%
-          (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
-            (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
-              (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
-                (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3) %% prf4) =
+      | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
+        (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %%
+          (PAxm ("Pure.symmetric", _, _) % _ % _ %%
+            (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
+              (PAxm ("Pure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
+                (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3) %% prf4) =
           SOME (equal_elim_axm %> D %> C %% (symmetric_axm % ?? C % ?? D %% prf2) %%
             (equal_elim_axm %> B %> D %% prf3 %%
               (equal_elim_axm %> A %> B %% prf1 %% prf4)))
 
-      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
-        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
-          (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %%
-            (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
-              (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
-                (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
-                  (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3)) %% prf4) =
+      | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
+        (PAxm ("Pure.symmetric", _, _) % _ % _ %%
+          (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %%
+            (PAxm ("Pure.symmetric", _, _) % _ % _ %%
+              (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
+                (PAxm ("Pure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
+                  (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3)) %% prf4) =
           SOME (equal_elim_axm %> B %> A %% (symmetric_axm % ?? A % ?? B %% prf1) %%
             (equal_elim_axm %> D %> B %% (symmetric_axm % ?? B % ?? D %% prf3) %%
               (equal_elim_axm %> C %> D %% prf2 %% prf4)))
 
-      | rew' ((prf as PAxm ("ProtoPure.combination", _, _) %
+      | rew' ((prf as PAxm ("Pure.combination", _, _) %
         SOME ((eq as Const ("==", T)) $ t) % _ % _ % _) %%
-          (PAxm ("ProtoPure.reflexive", _, _) % _)) =
+          (PAxm ("Pure.reflexive", _, _) % _)) =
         let val (U, V) = (case T of
           Type (_, [U, V]) => (U, V) | _ => (dummyT, dummyT))
         in SOME (prf %% (ax combination_axm [V, U] %> eq % ?? eq % ?? t % ?? t %%

--- a/src/Pure/Syntax/syn_trans.ML	Thu Mar 27 14:41:07 2008 +0100
+++ b/src/Pure/Syntax/syn_trans.ML	Thu Mar 27 14:41:09 2008 +0100
@@ -149,7 +149,7 @@
 
 (* meta conjunction *)
 
-fun conjunction_tr [t, u] = Lexicon.const "ProtoPure.conjunction" $ t $ u
+fun conjunction_tr [t, u] = Lexicon.const "Pure.conjunction" $ t $ u
   | conjunction_tr ts = raise TERM ("conjunction_tr", ts);
 
 
@@ -159,7 +159,7 @@
       Lexicon.const "_constrain" $ Lexicon.const "TYPE" $ (Lexicon.const "itself" $ ty)
   | type_tr (*"_TYPE"*) ts = raise TERM ("type_tr", ts);
 
-fun term_tr [t] = Lexicon.const "ProtoPure.term" $ t
+fun term_tr [t] = Lexicon.const "Pure.term" $ t
   | term_tr ts = raise TERM ("term_tr", ts);
 
 
@@ -341,7 +341,7 @@
     fun is_prop Ts t =
       fastype_of1 (Ts, t) = propT handle TERM _ => false;
 
-    fun is_term (Const ("ProtoPure.term", _) $ _) = true
+    fun is_term (Const ("Pure.term", _) $ _) = true
       | is_term _ = false;
 
     fun tr' _ (t as Const _) = t

--- a/src/Pure/conjunction.ML	Thu Mar 27 14:41:07 2008 +0100
+++ b/src/Pure/conjunction.ML	Thu Mar 27 14:41:09 2008 +0100
@@ -29,7 +29,7 @@
 
 (** abstract syntax **)
 
-val cert = Thm.cterm_of ProtoPure.thy;
+val cert = Thm.cterm_of (Context.the_theory (Context.the_thread_data ()));
 val read_prop = cert o SimpleSyntax.read_prop;
 
 val true_prop = cert Logic.true_prop;
@@ -42,7 +42,7 @@
 
 fun dest_conjunction ct =
   (case Thm.term_of ct of
-    (Const ("ProtoPure.conjunction", _) $ _ $ _) => Thm.dest_binop ct
+    (Const ("Pure.conjunction", _) $ _ $ _) => Thm.dest_binop ct
   | _ => raise TERM ("dest_conjunction", [Thm.term_of ct]));
 
 
@@ -69,7 +69,8 @@
 val ABC = read_prop "A ==> B ==> C";
 val A_B = read_prop "A && B";
 
-val conjunction_def = Thm.unvarify ProtoPure.conjunction_def;
+val conjunction_def =
+  Thm.unvarify (Thm.get_axiom (Context.the_theory (Context.the_thread_data ())) "conjunction_def");
 
 fun conjunctionD which =
   Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP
@@ -121,8 +122,8 @@
 
 local
 
-fun conjs n =
-  let val As = map (fn A => cert (Free (A, propT))) (Name.invents Name.context "A" n)
+fun conjs thy n =
+  let val As = map (fn A => Thm.cterm_of thy (Free (A, propT))) (Name.invents Name.context "A" n)
   in (As, mk_conjunction_balanced As) end;
 
 val B = read_prop "B";
@@ -142,7 +143,8 @@
   if n < 2 then th
   else
     let
-      val (As, C) = conjs n;
+      val thy = Thm.theory_of_thm th;
+      val (As, C) = conjs thy n;
       val D = Drule.mk_implies (C, B);
     in
       comp_rule th
@@ -159,7 +161,8 @@
   if n < 2 then th
   else
     let
-      val (As, C) = conjs n;
+      val thy = Thm.theory_of_thm th;
+      val (As, C) = conjs thy n;
       val D = Drule.list_implies (As, B);
     in
       comp_rule th

--- a/src/Pure/drule.ML	Thu Mar 27 14:41:07 2008 +0100
+++ b/src/Pure/drule.ML	Thu Mar 27 14:41:09 2008 +0100
@@ -160,7 +160,7 @@
   let val {T, thy, ...} = Thm.rep_ctyp cT
   in Thm.ctyp_of thy (f T) end;
 
-val cert = cterm_of ProtoPure.thy;
+val cert = cterm_of (Context.the_theory (Context.the_thread_data ()));
 
 val implies = cert Term.implies;
 fun mk_implies (A, B) = Thm.capply (Thm.capply implies A) B;
@@ -518,7 +518,7 @@
 
 (*** Meta-Rewriting Rules ***)
 
-val read_prop = Thm.cterm_of ProtoPure.thy o SimpleSyntax.read_prop;
+val read_prop = cert o SimpleSyntax.read_prop;
 
 fun store_thm name thm = hd (PureThy.smart_store_thms (name, [thm]));
 fun store_standard_thm name thm = store_thm name (standard thm);
@@ -858,8 +858,9 @@
 
 local
   val A = cert (Free ("A", propT));
-  val prop_def = Thm.unvarify ProtoPure.prop_def;
-  val term_def = Thm.unvarify ProtoPure.term_def;
+  val get_axiom = Thm.unvarify o Thm.get_axiom (Context.the_theory (Context.the_thread_data ()));
+  val prop_def = get_axiom "prop_def";
+  val term_def = get_axiom "term_def";
 in
   val protect = Thm.capply (cert Logic.protectC);
   val protectI = store_thm "protectI" (PureThy.kind_rule Thm.internalK (standard
@@ -899,7 +900,7 @@
 fun cterm_rule f = dest_term o f o mk_term;
 fun term_rule thy f t = Thm.term_of (cterm_rule f (Thm.cterm_of thy t));
 
-val dummy_thm = mk_term (Thm.cterm_of ProtoPure.thy (Term.dummy_pattern propT));
+val dummy_thm = mk_term (cert (Term.dummy_pattern propT));
 
 
 

--- a/src/Pure/logic.ML	Thu Mar 27 14:41:07 2008 +0100
+++ b/src/Pure/logic.ML	Thu Mar 27 14:41:09 2008 +0100
@@ -145,7 +145,7 @@
 (** conjunction **)
 
 val true_prop = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0));
-val conjunction = Const ("ProtoPure.conjunction", propT --> propT --> propT);
+val conjunction = Const ("Pure.conjunction", propT --> propT --> propT);
 
 
 (*A && B*)
@@ -161,7 +161,7 @@
 
 
 (*A && B*)
-fun dest_conjunction (Const ("ProtoPure.conjunction", _) $ A $ B) = (A, B)
+fun dest_conjunction (Const ("Pure.conjunction", _) $ A $ B) = (A, B)
   | dest_conjunction t = raise TERM ("dest_conjunction", [t]);
 
 (*A && B && C -- improper*)
@@ -264,9 +264,9 @@
   | unprotect t = raise TERM ("unprotect", [t]);
 
 
-fun mk_term t = Const ("ProtoPure.term", Term.fastype_of t --> propT) $ t;
+fun mk_term t = Const ("Pure.term", Term.fastype_of t --> propT) $ t;
 
-fun dest_term (Const ("ProtoPure.term", _) $ t) = t
+fun dest_term (Const ("Pure.term", _) $ t) = t
   | dest_term t = raise TERM ("dest_term", [t]);
 
 

--- a/src/Pure/meta_simplifier.ML	Thu Mar 27 14:41:07 2008 +0100
+++ b/src/Pure/meta_simplifier.ML	Thu Mar 27 14:41:09 2008 +0100
@@ -1332,16 +1332,17 @@
 
 fun gen_norm_hhf ss th =
   (if Drule.is_norm_hhf (Thm.prop_of th) then th
-   else Conv.fconv_rule (rewrite_cterm (true, false, false) (K (K NONE)) ss) th)
+   else Conv.fconv_rule
+    (rewrite_cterm (true, false, false) (K (K NONE)) (theory_context (Thm.theory_of_thm th) ss)) th)
   |> Thm.adjust_maxidx_thm ~1
   |> Drule.gen_all;
 
-val ss = theory_context ProtoPure.thy empty_ss addsimps [Drule.norm_hhf_eq];
+val hhf_ss = empty_ss addsimps [Drule.norm_hhf_eq];
 
 in
 
-val norm_hhf = gen_norm_hhf ss;
-val norm_hhf_protect = gen_norm_hhf (ss addeqcongs [Drule.protect_cong]);
+val norm_hhf = gen_norm_hhf hhf_ss;
+val norm_hhf_protect = gen_norm_hhf (hhf_ss addeqcongs [Drule.protect_cong]);
 
 end;
 

--- a/src/Pure/proofterm.ML	Thu Mar 27 14:41:07 2008 +0100
+++ b/src/Pure/proofterm.ML	Thu Mar 27 14:41:09 2008 +0100
@@ -784,17 +784,17 @@
 
 val [reflexive_axm, symmetric_axm, transitive_axm, equal_intr_axm,
   equal_elim_axm, abstract_rule_axm, combination_axm] =
-    map (fn (s, t) => PAxm ("ProtoPure." ^ s, varify t, NONE)) equality_axms;
+    map (fn (s, t) => PAxm ("Pure." ^ s, varify t, NONE)) equality_axms;
 
 end;
 
 val reflexive = reflexive_axm % NONE;
 
-fun symmetric (prf as PAxm ("ProtoPure.reflexive", _, _) % _) = prf
+fun symmetric (prf as PAxm ("Pure.reflexive", _, _) % _) = prf
   | symmetric prf = symmetric_axm % NONE % NONE %% prf;
 
-fun transitive _ _ (PAxm ("ProtoPure.reflexive", _, _) % _) prf2 = prf2
-  | transitive _ _ prf1 (PAxm ("ProtoPure.reflexive", _, _) % _) = prf1
+fun transitive _ _ (PAxm ("Pure.reflexive", _, _) % _) prf2 = prf2
+  | transitive _ _ prf1 (PAxm ("Pure.reflexive", _, _) % _) = prf1
   | transitive u (Type ("prop", [])) prf1 prf2 =
       transitive_axm % NONE % SOME (remove_types u) % NONE %% prf1 %% prf2
   | transitive u T prf1 prf2 =
@@ -803,11 +803,11 @@
 fun abstract_rule x a prf =
   abstract_rule_axm % NONE % NONE %% forall_intr_proof x a prf;
 
-fun check_comb (PAxm ("ProtoPure.combination", _, _) % f % g % _ % _ %% prf %% _) =
+fun check_comb (PAxm ("Pure.combination", _, _) % f % g % _ % _ %% prf %% _) =
       is_some f orelse check_comb prf
-  | check_comb (PAxm ("ProtoPure.transitive", _, _) % _ % _ % _ %% prf1 %% prf2) =
+  | check_comb (PAxm ("Pure.transitive", _, _) % _ % _ % _ %% prf1 %% prf2) =
       check_comb prf1 andalso check_comb prf2
-  | check_comb (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% prf) = check_comb prf
+  | check_comb (PAxm ("Pure.symmetric", _, _) % _ % _ %% prf) = check_comb prf
   | check_comb _ = false;
 
 fun combination f g t u (Type (_, [T, U])) prf1 prf2 =
@@ -817,7 +817,7 @@
     val prf =  if check_comb prf1 then
         combination_axm % NONE % NONE
       else (case prf1 of
-          PAxm ("ProtoPure.reflexive", _, _) % _ =>
+          PAxm ("Pure.reflexive", _, _) % _ =>
             combination_axm %> remove_types f % NONE
         | _ => combination_axm %> remove_types f %> remove_types g)
   in

--- a/src/Pure/tactic.ML	Thu Mar 27 14:41:07 2008 +0100
+++ b/src/Pure/tactic.ML	Thu Mar 27 14:41:09 2008 +0100
@@ -315,8 +315,9 @@
 (*For forw_inst_tac and dres_inst_tac.  Preserve Var indexes of rl;
   increment revcut_rl instead.*)
 fun make_elim_preserve rl =
-  let val {maxidx,...} = rep_thm rl
-      fun cvar ixn = cterm_of ProtoPure.thy (Var(ixn,propT));
+  let val maxidx = Thm.maxidx_of rl
+      val thy = Thm.theory_of_thm rl
+      fun cvar ixn = cterm_of thy (Var(ixn,propT));
       val revcut_rl' =
           instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
                              (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl

--- a/src/Pure/thm.ML	Thu Mar 27 14:41:07 2008 +0100
+++ b/src/Pure/thm.ML	Thu Mar 27 14:41:09 2008 +0100
@@ -1146,7 +1146,7 @@
     val Cterm {t, maxidx, sorts, ...} =
       cterm_of thy (Logic.mk_inclass (TVar ((Name.aT, 0), [c]), Sign.certify_class thy c))
         handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
-    val der = Pt.infer_derivs' I (false, Pt.PAxm ("ProtoPure.class_triv:" ^ c, t, SOME []));
+    val der = Pt.infer_derivs' I (false, Pt.PAxm ("Pure.class_triv:" ^ c, t, SOME []));
   in
     Thm {thy_ref = Theory.check_thy thy, der = der, tags = [], maxidx = maxidx,
       shyps = sorts, hyps = [], tpairs = [], prop = t}
@@ -1164,7 +1164,7 @@
     val constraints = map (curry Logic.mk_inclass T') S;
   in
     Thm {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
-      der = Pt.infer_derivs' I (false, Pt.PAxm ("ProtoPure.unconstrainT", prop, SOME [])),
+      der = Pt.infer_derivs' I (false, Pt.PAxm ("Pure.unconstrainT", prop, SOME [])),
       tags = [],
       maxidx = Int.max (maxidx, i),
       shyps = Sorts.remove_sort S shyps,