eliminated theory ProtoPure;
authorwenzelm
Thu Mar 27 14:41:09 2008 +0100 (2008-03-27)
changeset 26424a6cad32a27b0
parent 26423 8408edac8f6b
child 26425 6561665c5cb1
eliminated theory ProtoPure;
src/HOL/Import/shuffler.ML
src/HOL/Tools/ComputeHOL.thy
src/HOL/Tools/meson.ML
src/Pure/Isar/local_defs.ML
src/Pure/Proof/proof_rewrite_rules.ML
src/Pure/Syntax/syn_trans.ML
src/Pure/conjunction.ML
src/Pure/drule.ML
src/Pure/logic.ML
src/Pure/meta_simplifier.ML
src/Pure/proofterm.ML
src/Pure/tactic.ML
src/Pure/thm.ML
     1.1 --- a/src/HOL/Import/shuffler.ML	Thu Mar 27 14:41:07 2008 +0100
     1.2 +++ b/src/HOL/Import/shuffler.ML	Thu Mar 27 14:41:09 2008 +0100
     1.3 @@ -90,7 +90,7 @@
     1.4  
     1.5  val weaken =
     1.6      let
     1.7 -        val cert = cterm_of ProtoPure.thy
     1.8 +        val cert = cterm_of Pure.thy
     1.9          val P = Free("P",propT)
    1.10          val Q = Free("Q",propT)
    1.11          val PQ = Logic.mk_implies(P,Q)
    1.12 @@ -109,7 +109,7 @@
    1.13  
    1.14  val imp_comm =
    1.15      let
    1.16 -        val cert = cterm_of ProtoPure.thy
    1.17 +        val cert = cterm_of Pure.thy
    1.18          val P = Free("P",propT)
    1.19          val Q = Free("Q",propT)
    1.20          val R = Free("R",propT)
    1.21 @@ -129,7 +129,7 @@
    1.22  
    1.23  val def_norm =
    1.24      let
    1.25 -        val cert = cterm_of ProtoPure.thy
    1.26 +        val cert = cterm_of Pure.thy
    1.27          val aT = TFree("'a",[])
    1.28          val bT = TFree("'b",[])
    1.29          val v = Free("v",aT)
    1.30 @@ -156,7 +156,7 @@
    1.31  
    1.32  val all_comm =
    1.33      let
    1.34 -        val cert = cterm_of ProtoPure.thy
    1.35 +        val cert = cterm_of Pure.thy
    1.36          val xT = TFree("'a",[])
    1.37          val yT = TFree("'b",[])
    1.38          val P = Free("P",xT-->yT-->propT)
    1.39 @@ -180,7 +180,7 @@
    1.40  
    1.41  val equiv_comm =
    1.42      let
    1.43 -        val cert = cterm_of ProtoPure.thy
    1.44 +        val cert = cterm_of Pure.thy
    1.45          val T    = TFree("'a",[])
    1.46          val t    = Free("t",T)
    1.47          val u    = Free("u",T)
     2.1 --- a/src/HOL/Tools/ComputeHOL.thy	Thu Mar 27 14:41:07 2008 +0100
     2.2 +++ b/src/HOL/Tools/ComputeHOL.thy	Thu Mar 27 14:41:09 2008 +0100
     2.3 @@ -172,12 +172,7 @@
     2.4  
     2.5  fun prep_thms ths = map (convert_conditions o to_meta_eq) ths
     2.6  
     2.7 -local
     2.8 -    val sym_HOL = @{thm "HOL.sym"}
     2.9 -    val sym_Pure = @{thm "ProtoPure.symmetric"}
    2.10 -in
    2.11 -  fun symmetric th = ((sym_HOL OF [th]) handle THM _ => (sym_Pure OF [th]))
    2.12 -end
    2.13 +fun symmetric th = @{thm "HOL.sym"} OF [th] handle THM _ => @{thm "Pure.symmetric"} OF [th]
    2.14  
    2.15  local
    2.16      val trans_HOL = @{thm "HOL.trans"}
     3.1 --- a/src/HOL/Tools/meson.ML	Thu Mar 27 14:41:07 2008 +0100
     3.2 +++ b/src/HOL/Tools/meson.ML	Thu Mar 27 14:41:09 2008 +0100
     3.3 @@ -291,7 +291,7 @@
     3.4  fun resop nf [prem] = resolve_tac (nf prem) 1;
     3.5  
     3.6  (*Any need to extend this list with
     3.7 -  "HOL.type_class","HOL.eq_class","ProtoPure.term"?*)
     3.8 +  "HOL.type_class","HOL.eq_class","Pure.term"?*)
     3.9  val has_meta_conn =
    3.10      exists_Const (member (op =) ["==", "==>", "all", "prop"] o #1);
    3.11  
     4.1 --- a/src/Pure/Isar/local_defs.ML	Thu Mar 27 14:41:07 2008 +0100
     4.2 +++ b/src/Pure/Isar/local_defs.ML	Thu Mar 27 14:41:09 2008 +0100
     4.3 @@ -203,13 +203,11 @@
     4.4  
     4.5  (* meta rewrite rules *)
     4.6  
     4.7 -val equals_ss =
     4.8 -  MetaSimplifier.theory_context ProtoPure.thy MetaSimplifier.empty_ss
     4.9 -    addeqcongs [Drule.equals_cong];    (*protect meta-level equality*)
    4.10 -
    4.11  fun meta_rewrite_conv ctxt =
    4.12    MetaSimplifier.rewrite_cterm (false, false, false) (K (K NONE))
    4.13 -    (equals_ss addsimps (Rules.get (Context.Proof ctxt)));
    4.14 +    (MetaSimplifier.context ctxt MetaSimplifier.empty_ss
    4.15 +      addeqcongs [Drule.equals_cong]    (*protect meta-level equality*)
    4.16 +      addsimps (Rules.get (Context.Proof ctxt)));
    4.17  
    4.18  val meta_rewrite_rule = Conv.fconv_rule o meta_rewrite_conv;
    4.19  
     5.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Thu Mar 27 14:41:07 2008 +0100
     5.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Thu Mar 27 14:41:09 2008 +0100
     5.3 @@ -34,36 +34,36 @@
     5.4      val equal_elim_axm = ax equal_elim_axm [];
     5.5      val symmetric_axm = ax symmetric_axm [propT];
     5.6  
     5.7 -    fun rew' (PThm ("ProtoPure.protectD", _, _, _) % _ %%
     5.8 -        (PThm ("ProtoPure.protectI", _, _, _) % _ %% prf)) = SOME prf
     5.9 -      | rew' (PThm ("ProtoPure.conjunctionD1", _, _, _) % _ % _ %%
    5.10 -        (PThm ("ProtoPure.conjunctionI", _, _, _) % _ % _ %% prf %% _)) = SOME prf
    5.11 -      | rew' (PThm ("ProtoPure.conjunctionD2", _, _, _) % _ % _ %%
    5.12 -        (PThm ("ProtoPure.conjunctionI", _, _, _) % _ % _ %% _ %% prf)) = SOME prf
    5.13 -      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
    5.14 -        (PAxm ("ProtoPure.equal_intr", _, _) % _ % _ %% prf %% _)) = SOME prf
    5.15 -      | rew' (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
    5.16 -        (PAxm ("ProtoPure.equal_intr", _, _) % A % B %% prf1 %% prf2)) =
    5.17 +    fun rew' (PThm ("Pure.protectD", _, _, _) % _ %%
    5.18 +        (PThm ("Pure.protectI", _, _, _) % _ %% prf)) = SOME prf
    5.19 +      | rew' (PThm ("Pure.conjunctionD1", _, _, _) % _ % _ %%
    5.20 +        (PThm ("Pure.conjunctionI", _, _, _) % _ % _ %% prf %% _)) = SOME prf
    5.21 +      | rew' (PThm ("Pure.conjunctionD2", _, _, _) % _ % _ %%
    5.22 +        (PThm ("Pure.conjunctionI", _, _, _) % _ % _ %% _ %% prf)) = SOME prf
    5.23 +      | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
    5.24 +        (PAxm ("Pure.equal_intr", _, _) % _ % _ %% prf %% _)) = SOME prf
    5.25 +      | rew' (PAxm ("Pure.symmetric", _, _) % _ % _ %%
    5.26 +        (PAxm ("Pure.equal_intr", _, _) % A % B %% prf1 %% prf2)) =
    5.27              SOME (equal_intr_axm % B % A %% prf2 %% prf1)
    5.28  
    5.29 -      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
    5.30 -        (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("prop", _)) %
    5.31 -          _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %%
    5.32 -        ((tg as PThm ("ProtoPure.protectI", _, _, _)) % _ %% prf2)) =
    5.33 +      | rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
    5.34 +        (PAxm ("Pure.combination", _, _) % SOME (Const ("prop", _)) %
    5.35 +          _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %%
    5.36 +        ((tg as PThm ("Pure.protectI", _, _, _)) % _ %% prf2)) =
    5.37          SOME (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
    5.38  
    5.39 -      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
    5.40 -        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
    5.41 -          (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("prop", _)) %
    5.42 -             _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1)) %%
    5.43 -        ((tg as PThm ("ProtoPure.protectI", _, _, _)) % _ %% prf2)) =
    5.44 +      | rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
    5.45 +        (PAxm ("Pure.symmetric", _, _) % _ % _ %%
    5.46 +          (PAxm ("Pure.combination", _, _) % SOME (Const ("prop", _)) %
    5.47 +             _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1)) %%
    5.48 +        ((tg as PThm ("Pure.protectI", _, _, _)) % _ %% prf2)) =
    5.49          SOME (tg %> B %% (equal_elim_axm %> A %> B %%
    5.50            (symmetric_axm % ?? B % ?? A %% prf1) %% prf2))
    5.51  
    5.52 -      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME X % SOME Y %%
    5.53 -        (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
    5.54 -          (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==>", _)) % _ % _ % _ %%
    5.55 -             (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) =
    5.56 +      | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
    5.57 +        (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
    5.58 +          (PAxm ("Pure.combination", _, _) % SOME (Const ("==>", _)) % _ % _ % _ %%
    5.59 +             (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2)) =
    5.60          let
    5.61            val _ $ A $ C = Envir.beta_norm X;
    5.62            val _ $ B $ D = Envir.beta_norm Y
    5.63 @@ -73,11 +73,11 @@
    5.64                (symmetric_axm % ?? A % ?? B %% incr_pboundvars 2 0 prf1) %% PBound 0)))))
    5.65          end
    5.66  
    5.67 -      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME X % SOME Y %%
    5.68 -        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
    5.69 -          (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
    5.70 -            (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==>", _)) % _ % _ % _ %%
    5.71 -               (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2))) =
    5.72 +      | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
    5.73 +        (PAxm ("Pure.symmetric", _, _) % _ % _ %%
    5.74 +          (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
    5.75 +            (PAxm ("Pure.combination", _, _) % SOME (Const ("==>", _)) % _ % _ % _ %%
    5.76 +               (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2))) =
    5.77          let
    5.78            val _ $ A $ C = Envir.beta_norm Y;
    5.79            val _ $ B $ D = Envir.beta_norm X
    5.80 @@ -87,10 +87,10 @@
    5.81                %% (PBound 1 %% (equal_elim_axm %> A %> B %% incr_pboundvars 2 0 prf1 %% PBound 0)))))
    5.82          end
    5.83  
    5.84 -      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME X % SOME Y %%
    5.85 -        (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("all", _)) % _ % _ % _ %%
    5.86 -          (PAxm ("ProtoPure.reflexive", _, _) % _) %%
    5.87 -            (PAxm ("ProtoPure.abstract_rule", _, _) % _ % _ %% prf))) =
    5.88 +      | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
    5.89 +        (PAxm ("Pure.combination", _, _) % SOME (Const ("all", _)) % _ % _ % _ %%
    5.90 +          (PAxm ("Pure.reflexive", _, _) % _) %%
    5.91 +            (PAxm ("Pure.abstract_rule", _, _) % _ % _ %% prf))) =
    5.92          let
    5.93            val Const (_, T) $ P = Envir.beta_norm X;
    5.94            val _ $ Q = Envir.beta_norm Y;
    5.95 @@ -99,11 +99,11 @@
    5.96                (incr_pboundvars 1 1 prf %> Bound 0) %% (PBound 0 %> Bound 0))))
    5.97          end
    5.98  
    5.99 -      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME X % SOME Y %%
   5.100 -        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%        
   5.101 -          (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("all", _)) % _ % _ % _ %%
   5.102 -            (PAxm ("ProtoPure.reflexive", _, _) % _) %%
   5.103 -              (PAxm ("ProtoPure.abstract_rule", _, _) % _ % _ %% prf)))) =
   5.104 +      | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
   5.105 +        (PAxm ("Pure.symmetric", _, _) % _ % _ %%        
   5.106 +          (PAxm ("Pure.combination", _, _) % SOME (Const ("all", _)) % _ % _ % _ %%
   5.107 +            (PAxm ("Pure.reflexive", _, _) % _) %%
   5.108 +              (PAxm ("Pure.abstract_rule", _, _) % _ % _ %% prf)))) =
   5.109          let
   5.110            val Const (_, T) $ P = Envir.beta_norm X;
   5.111            val _ $ Q = Envir.beta_norm Y;
   5.112 @@ -115,68 +115,68 @@
   5.113                %% (PBound 0 %> Bound 0))))
   5.114          end
   5.115  
   5.116 -      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME A % SOME C %%
   5.117 -        (PAxm ("ProtoPure.transitive", _, _) % _ % SOME B % _ %% prf1 %% prf2) %% prf3) =
   5.118 +      | rew' (PAxm ("Pure.equal_elim", _, _) % SOME A % SOME C %%
   5.119 +        (PAxm ("Pure.transitive", _, _) % _ % SOME B % _ %% prf1 %% prf2) %% prf3) =
   5.120             SOME (equal_elim_axm %> B %> C %% prf2 %%
   5.121               (equal_elim_axm %> A %> B %% prf1 %% prf3))
   5.122 -      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME A % SOME C %%
   5.123 -        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
   5.124 -          (PAxm ("ProtoPure.transitive", _, _) % _ % SOME B % _ %% prf1 %% prf2)) %% prf3) =
   5.125 +      | rew' (PAxm ("Pure.equal_elim", _, _) % SOME A % SOME C %%
   5.126 +        (PAxm ("Pure.symmetric", _, _) % _ % _ %%
   5.127 +          (PAxm ("Pure.transitive", _, _) % _ % SOME B % _ %% prf1 %% prf2)) %% prf3) =
   5.128             SOME (equal_elim_axm %> B %> C %% (symmetric_axm % ?? C % ?? B %% prf1) %%
   5.129               (equal_elim_axm %> A %> B %% (symmetric_axm % ?? B % ?? A %% prf2) %% prf3))
   5.130  
   5.131 -      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
   5.132 -        (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf) = SOME prf
   5.133 -      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
   5.134 -        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
   5.135 -          (PAxm ("ProtoPure.reflexive", _, _) % _)) %% prf) = SOME prf
   5.136 +      | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
   5.137 +        (PAxm ("Pure.reflexive", _, _) % _) %% prf) = SOME prf
   5.138 +      | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
   5.139 +        (PAxm ("Pure.symmetric", _, _) % _ % _ %%
   5.140 +          (PAxm ("Pure.reflexive", _, _) % _)) %% prf) = SOME prf
   5.141  
   5.142 -      | rew' (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
   5.143 -        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% prf)) = SOME prf
   5.144 +      | rew' (PAxm ("Pure.symmetric", _, _) % _ % _ %%
   5.145 +        (PAxm ("Pure.symmetric", _, _) % _ % _ %% prf)) = SOME prf
   5.146  
   5.147 -      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
   5.148 -        (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %%
   5.149 -          (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
   5.150 -            (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
   5.151 -              (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3) %% prf4) =
   5.152 +      | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
   5.153 +        (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %%
   5.154 +          (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
   5.155 +            (PAxm ("Pure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
   5.156 +              (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3) %% prf4) =
   5.157            SOME (equal_elim_axm %> C %> D %% prf2 %%
   5.158              (equal_elim_axm %> A %> C %% prf3 %%
   5.159                (equal_elim_axm %> B %> A %% (symmetric_axm % ?? A % ?? B %% prf1) %% prf4)))
   5.160  
   5.161 -      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
   5.162 -        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
   5.163 -          (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %%
   5.164 -            (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
   5.165 -              (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
   5.166 -                (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3)) %% prf4) =
   5.167 +      | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
   5.168 +        (PAxm ("Pure.symmetric", _, _) % _ % _ %%
   5.169 +          (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %%
   5.170 +            (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
   5.171 +              (PAxm ("Pure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
   5.172 +                (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3)) %% prf4) =
   5.173            SOME (equal_elim_axm %> A %> B %% prf1 %%
   5.174              (equal_elim_axm %> C %> A %% (symmetric_axm % ?? A % ?? C %% prf3) %%
   5.175                (equal_elim_axm %> D %> C %% (symmetric_axm % ?? C % ?? D %% prf2) %% prf4)))
   5.176  
   5.177 -      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
   5.178 -        (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %%
   5.179 -          (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
   5.180 -            (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
   5.181 -              (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
   5.182 -                (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3) %% prf4) =
   5.183 +      | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
   5.184 +        (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %%
   5.185 +          (PAxm ("Pure.symmetric", _, _) % _ % _ %%
   5.186 +            (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
   5.187 +              (PAxm ("Pure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
   5.188 +                (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3) %% prf4) =
   5.189            SOME (equal_elim_axm %> D %> C %% (symmetric_axm % ?? C % ?? D %% prf2) %%
   5.190              (equal_elim_axm %> B %> D %% prf3 %%
   5.191                (equal_elim_axm %> A %> B %% prf1 %% prf4)))
   5.192  
   5.193 -      | rew' (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
   5.194 -        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
   5.195 -          (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %%
   5.196 -            (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
   5.197 -              (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
   5.198 -                (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
   5.199 -                  (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3)) %% prf4) =
   5.200 +      | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
   5.201 +        (PAxm ("Pure.symmetric", _, _) % _ % _ %%
   5.202 +          (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %%
   5.203 +            (PAxm ("Pure.symmetric", _, _) % _ % _ %%
   5.204 +              (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
   5.205 +                (PAxm ("Pure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
   5.206 +                  (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3)) %% prf4) =
   5.207            SOME (equal_elim_axm %> B %> A %% (symmetric_axm % ?? A % ?? B %% prf1) %%
   5.208              (equal_elim_axm %> D %> B %% (symmetric_axm % ?? B % ?? D %% prf3) %%
   5.209                (equal_elim_axm %> C %> D %% prf2 %% prf4)))
   5.210  
   5.211 -      | rew' ((prf as PAxm ("ProtoPure.combination", _, _) %
   5.212 +      | rew' ((prf as PAxm ("Pure.combination", _, _) %
   5.213          SOME ((eq as Const ("==", T)) $ t) % _ % _ % _) %%
   5.214 -          (PAxm ("ProtoPure.reflexive", _, _) % _)) =
   5.215 +          (PAxm ("Pure.reflexive", _, _) % _)) =
   5.216          let val (U, V) = (case T of
   5.217            Type (_, [U, V]) => (U, V) | _ => (dummyT, dummyT))
   5.218          in SOME (prf %% (ax combination_axm [V, U] %> eq % ?? eq % ?? t % ?? t %%
     6.1 --- a/src/Pure/Syntax/syn_trans.ML	Thu Mar 27 14:41:07 2008 +0100
     6.2 +++ b/src/Pure/Syntax/syn_trans.ML	Thu Mar 27 14:41:09 2008 +0100
     6.3 @@ -149,7 +149,7 @@
     6.4  
     6.5  (* meta conjunction *)
     6.6  
     6.7 -fun conjunction_tr [t, u] = Lexicon.const "ProtoPure.conjunction" $ t $ u
     6.8 +fun conjunction_tr [t, u] = Lexicon.const "Pure.conjunction" $ t $ u
     6.9    | conjunction_tr ts = raise TERM ("conjunction_tr", ts);
    6.10  
    6.11  
    6.12 @@ -159,7 +159,7 @@
    6.13        Lexicon.const "_constrain" $ Lexicon.const "TYPE" $ (Lexicon.const "itself" $ ty)
    6.14    | type_tr (*"_TYPE"*) ts = raise TERM ("type_tr", ts);
    6.15  
    6.16 -fun term_tr [t] = Lexicon.const "ProtoPure.term" $ t
    6.17 +fun term_tr [t] = Lexicon.const "Pure.term" $ t
    6.18    | term_tr ts = raise TERM ("term_tr", ts);
    6.19  
    6.20  
    6.21 @@ -341,7 +341,7 @@
    6.22      fun is_prop Ts t =
    6.23        fastype_of1 (Ts, t) = propT handle TERM _ => false;
    6.24  
    6.25 -    fun is_term (Const ("ProtoPure.term", _) $ _) = true
    6.26 +    fun is_term (Const ("Pure.term", _) $ _) = true
    6.27        | is_term _ = false;
    6.28  
    6.29      fun tr' _ (t as Const _) = t
     7.1 --- a/src/Pure/conjunction.ML	Thu Mar 27 14:41:07 2008 +0100
     7.2 +++ b/src/Pure/conjunction.ML	Thu Mar 27 14:41:09 2008 +0100
     7.3 @@ -29,7 +29,7 @@
     7.4  
     7.5  (** abstract syntax **)
     7.6  
     7.7 -val cert = Thm.cterm_of ProtoPure.thy;
     7.8 +val cert = Thm.cterm_of (Context.the_theory (Context.the_thread_data ()));
     7.9  val read_prop = cert o SimpleSyntax.read_prop;
    7.10  
    7.11  val true_prop = cert Logic.true_prop;
    7.12 @@ -42,7 +42,7 @@
    7.13  
    7.14  fun dest_conjunction ct =
    7.15    (case Thm.term_of ct of
    7.16 -    (Const ("ProtoPure.conjunction", _) $ _ $ _) => Thm.dest_binop ct
    7.17 +    (Const ("Pure.conjunction", _) $ _ $ _) => Thm.dest_binop ct
    7.18    | _ => raise TERM ("dest_conjunction", [Thm.term_of ct]));
    7.19  
    7.20  
    7.21 @@ -69,7 +69,8 @@
    7.22  val ABC = read_prop "A ==> B ==> C";
    7.23  val A_B = read_prop "A && B";
    7.24  
    7.25 -val conjunction_def = Thm.unvarify ProtoPure.conjunction_def;
    7.26 +val conjunction_def =
    7.27 +  Thm.unvarify (Thm.get_axiom (Context.the_theory (Context.the_thread_data ())) "conjunction_def");
    7.28  
    7.29  fun conjunctionD which =
    7.30    Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP
    7.31 @@ -121,8 +122,8 @@
    7.32  
    7.33  local
    7.34  
    7.35 -fun conjs n =
    7.36 -  let val As = map (fn A => cert (Free (A, propT))) (Name.invents Name.context "A" n)
    7.37 +fun conjs thy n =
    7.38 +  let val As = map (fn A => Thm.cterm_of thy (Free (A, propT))) (Name.invents Name.context "A" n)
    7.39    in (As, mk_conjunction_balanced As) end;
    7.40  
    7.41  val B = read_prop "B";
    7.42 @@ -142,7 +143,8 @@
    7.43    if n < 2 then th
    7.44    else
    7.45      let
    7.46 -      val (As, C) = conjs n;
    7.47 +      val thy = Thm.theory_of_thm th;
    7.48 +      val (As, C) = conjs thy n;
    7.49        val D = Drule.mk_implies (C, B);
    7.50      in
    7.51        comp_rule th
    7.52 @@ -159,7 +161,8 @@
    7.53    if n < 2 then th
    7.54    else
    7.55      let
    7.56 -      val (As, C) = conjs n;
    7.57 +      val thy = Thm.theory_of_thm th;
    7.58 +      val (As, C) = conjs thy n;
    7.59        val D = Drule.list_implies (As, B);
    7.60      in
    7.61        comp_rule th
     8.1 --- a/src/Pure/drule.ML	Thu Mar 27 14:41:07 2008 +0100
     8.2 +++ b/src/Pure/drule.ML	Thu Mar 27 14:41:09 2008 +0100
     8.3 @@ -160,7 +160,7 @@
     8.4    let val {T, thy, ...} = Thm.rep_ctyp cT
     8.5    in Thm.ctyp_of thy (f T) end;
     8.6  
     8.7 -val cert = cterm_of ProtoPure.thy;
     8.8 +val cert = cterm_of (Context.the_theory (Context.the_thread_data ()));
     8.9  
    8.10  val implies = cert Term.implies;
    8.11  fun mk_implies (A, B) = Thm.capply (Thm.capply implies A) B;
    8.12 @@ -518,7 +518,7 @@
    8.13  
    8.14  (*** Meta-Rewriting Rules ***)
    8.15  
    8.16 -val read_prop = Thm.cterm_of ProtoPure.thy o SimpleSyntax.read_prop;
    8.17 +val read_prop = cert o SimpleSyntax.read_prop;
    8.18  
    8.19  fun store_thm name thm = hd (PureThy.smart_store_thms (name, [thm]));
    8.20  fun store_standard_thm name thm = store_thm name (standard thm);
    8.21 @@ -858,8 +858,9 @@
    8.22  
    8.23  local
    8.24    val A = cert (Free ("A", propT));
    8.25 -  val prop_def = Thm.unvarify ProtoPure.prop_def;
    8.26 -  val term_def = Thm.unvarify ProtoPure.term_def;
    8.27 +  val get_axiom = Thm.unvarify o Thm.get_axiom (Context.the_theory (Context.the_thread_data ()));
    8.28 +  val prop_def = get_axiom "prop_def";
    8.29 +  val term_def = get_axiom "term_def";
    8.30  in
    8.31    val protect = Thm.capply (cert Logic.protectC);
    8.32    val protectI = store_thm "protectI" (PureThy.kind_rule Thm.internalK (standard
    8.33 @@ -899,7 +900,7 @@
    8.34  fun cterm_rule f = dest_term o f o mk_term;
    8.35  fun term_rule thy f t = Thm.term_of (cterm_rule f (Thm.cterm_of thy t));
    8.36  
    8.37 -val dummy_thm = mk_term (Thm.cterm_of ProtoPure.thy (Term.dummy_pattern propT));
    8.38 +val dummy_thm = mk_term (cert (Term.dummy_pattern propT));
    8.39  
    8.40  
    8.41  
     9.1 --- a/src/Pure/logic.ML	Thu Mar 27 14:41:07 2008 +0100
     9.2 +++ b/src/Pure/logic.ML	Thu Mar 27 14:41:09 2008 +0100
     9.3 @@ -145,7 +145,7 @@
     9.4  (** conjunction **)
     9.5  
     9.6  val true_prop = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0));
     9.7 -val conjunction = Const ("ProtoPure.conjunction", propT --> propT --> propT);
     9.8 +val conjunction = Const ("Pure.conjunction", propT --> propT --> propT);
     9.9  
    9.10  
    9.11  (*A && B*)
    9.12 @@ -161,7 +161,7 @@
    9.13  
    9.14  
    9.15  (*A && B*)
    9.16 -fun dest_conjunction (Const ("ProtoPure.conjunction", _) $ A $ B) = (A, B)
    9.17 +fun dest_conjunction (Const ("Pure.conjunction", _) $ A $ B) = (A, B)
    9.18    | dest_conjunction t = raise TERM ("dest_conjunction", [t]);
    9.19  
    9.20  (*A && B && C -- improper*)
    9.21 @@ -264,9 +264,9 @@
    9.22    | unprotect t = raise TERM ("unprotect", [t]);
    9.23  
    9.24  
    9.25 -fun mk_term t = Const ("ProtoPure.term", Term.fastype_of t --> propT) $ t;
    9.26 +fun mk_term t = Const ("Pure.term", Term.fastype_of t --> propT) $ t;
    9.27  
    9.28 -fun dest_term (Const ("ProtoPure.term", _) $ t) = t
    9.29 +fun dest_term (Const ("Pure.term", _) $ t) = t
    9.30    | dest_term t = raise TERM ("dest_term", [t]);
    9.31  
    9.32  
    10.1 --- a/src/Pure/meta_simplifier.ML	Thu Mar 27 14:41:07 2008 +0100
    10.2 +++ b/src/Pure/meta_simplifier.ML	Thu Mar 27 14:41:09 2008 +0100
    10.3 @@ -1332,16 +1332,17 @@
    10.4  
    10.5  fun gen_norm_hhf ss th =
    10.6    (if Drule.is_norm_hhf (Thm.prop_of th) then th
    10.7 -   else Conv.fconv_rule (rewrite_cterm (true, false, false) (K (K NONE)) ss) th)
    10.8 +   else Conv.fconv_rule
    10.9 +    (rewrite_cterm (true, false, false) (K (K NONE)) (theory_context (Thm.theory_of_thm th) ss)) th)
   10.10    |> Thm.adjust_maxidx_thm ~1
   10.11    |> Drule.gen_all;
   10.12  
   10.13 -val ss = theory_context ProtoPure.thy empty_ss addsimps [Drule.norm_hhf_eq];
   10.14 +val hhf_ss = empty_ss addsimps [Drule.norm_hhf_eq];
   10.15  
   10.16  in
   10.17  
   10.18 -val norm_hhf = gen_norm_hhf ss;
   10.19 -val norm_hhf_protect = gen_norm_hhf (ss addeqcongs [Drule.protect_cong]);
   10.20 +val norm_hhf = gen_norm_hhf hhf_ss;
   10.21 +val norm_hhf_protect = gen_norm_hhf (hhf_ss addeqcongs [Drule.protect_cong]);
   10.22  
   10.23  end;
   10.24  
    11.1 --- a/src/Pure/proofterm.ML	Thu Mar 27 14:41:07 2008 +0100
    11.2 +++ b/src/Pure/proofterm.ML	Thu Mar 27 14:41:09 2008 +0100
    11.3 @@ -784,17 +784,17 @@
    11.4  
    11.5  val [reflexive_axm, symmetric_axm, transitive_axm, equal_intr_axm,
    11.6    equal_elim_axm, abstract_rule_axm, combination_axm] =
    11.7 -    map (fn (s, t) => PAxm ("ProtoPure." ^ s, varify t, NONE)) equality_axms;
    11.8 +    map (fn (s, t) => PAxm ("Pure." ^ s, varify t, NONE)) equality_axms;
    11.9  
   11.10  end;
   11.11  
   11.12  val reflexive = reflexive_axm % NONE;
   11.13  
   11.14 -fun symmetric (prf as PAxm ("ProtoPure.reflexive", _, _) % _) = prf
   11.15 +fun symmetric (prf as PAxm ("Pure.reflexive", _, _) % _) = prf
   11.16    | symmetric prf = symmetric_axm % NONE % NONE %% prf;
   11.17  
   11.18 -fun transitive _ _ (PAxm ("ProtoPure.reflexive", _, _) % _) prf2 = prf2
   11.19 -  | transitive _ _ prf1 (PAxm ("ProtoPure.reflexive", _, _) % _) = prf1
   11.20 +fun transitive _ _ (PAxm ("Pure.reflexive", _, _) % _) prf2 = prf2
   11.21 +  | transitive _ _ prf1 (PAxm ("Pure.reflexive", _, _) % _) = prf1
   11.22    | transitive u (Type ("prop", [])) prf1 prf2 =
   11.23        transitive_axm % NONE % SOME (remove_types u) % NONE %% prf1 %% prf2
   11.24    | transitive u T prf1 prf2 =
   11.25 @@ -803,11 +803,11 @@
   11.26  fun abstract_rule x a prf =
   11.27    abstract_rule_axm % NONE % NONE %% forall_intr_proof x a prf;
   11.28  
   11.29 -fun check_comb (PAxm ("ProtoPure.combination", _, _) % f % g % _ % _ %% prf %% _) =
   11.30 +fun check_comb (PAxm ("Pure.combination", _, _) % f % g % _ % _ %% prf %% _) =
   11.31        is_some f orelse check_comb prf
   11.32 -  | check_comb (PAxm ("ProtoPure.transitive", _, _) % _ % _ % _ %% prf1 %% prf2) =
   11.33 +  | check_comb (PAxm ("Pure.transitive", _, _) % _ % _ % _ %% prf1 %% prf2) =
   11.34        check_comb prf1 andalso check_comb prf2
   11.35 -  | check_comb (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% prf) = check_comb prf
   11.36 +  | check_comb (PAxm ("Pure.symmetric", _, _) % _ % _ %% prf) = check_comb prf
   11.37    | check_comb _ = false;
   11.38  
   11.39  fun combination f g t u (Type (_, [T, U])) prf1 prf2 =
   11.40 @@ -817,7 +817,7 @@
   11.41      val prf =  if check_comb prf1 then
   11.42          combination_axm % NONE % NONE
   11.43        else (case prf1 of
   11.44 -          PAxm ("ProtoPure.reflexive", _, _) % _ =>
   11.45 +          PAxm ("Pure.reflexive", _, _) % _ =>
   11.46              combination_axm %> remove_types f % NONE
   11.47          | _ => combination_axm %> remove_types f %> remove_types g)
   11.48    in
    12.1 --- a/src/Pure/tactic.ML	Thu Mar 27 14:41:07 2008 +0100
    12.2 +++ b/src/Pure/tactic.ML	Thu Mar 27 14:41:09 2008 +0100
    12.3 @@ -315,8 +315,9 @@
    12.4  (*For forw_inst_tac and dres_inst_tac.  Preserve Var indexes of rl;
    12.5    increment revcut_rl instead.*)
    12.6  fun make_elim_preserve rl =
    12.7 -  let val {maxidx,...} = rep_thm rl
    12.8 -      fun cvar ixn = cterm_of ProtoPure.thy (Var(ixn,propT));
    12.9 +  let val maxidx = Thm.maxidx_of rl
   12.10 +      val thy = Thm.theory_of_thm rl
   12.11 +      fun cvar ixn = cterm_of thy (Var(ixn,propT));
   12.12        val revcut_rl' =
   12.13            instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
   12.14                               (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
    13.1 --- a/src/Pure/thm.ML	Thu Mar 27 14:41:07 2008 +0100
    13.2 +++ b/src/Pure/thm.ML	Thu Mar 27 14:41:09 2008 +0100
    13.3 @@ -1146,7 +1146,7 @@
    13.4      val Cterm {t, maxidx, sorts, ...} =
    13.5        cterm_of thy (Logic.mk_inclass (TVar ((Name.aT, 0), [c]), Sign.certify_class thy c))
    13.6          handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
    13.7 -    val der = Pt.infer_derivs' I (false, Pt.PAxm ("ProtoPure.class_triv:" ^ c, t, SOME []));
    13.8 +    val der = Pt.infer_derivs' I (false, Pt.PAxm ("Pure.class_triv:" ^ c, t, SOME []));
    13.9    in
   13.10      Thm {thy_ref = Theory.check_thy thy, der = der, tags = [], maxidx = maxidx,
   13.11        shyps = sorts, hyps = [], tpairs = [], prop = t}
   13.12 @@ -1164,7 +1164,7 @@
   13.13      val constraints = map (curry Logic.mk_inclass T') S;
   13.14    in
   13.15      Thm {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
   13.16 -      der = Pt.infer_derivs' I (false, Pt.PAxm ("ProtoPure.unconstrainT", prop, SOME [])),
   13.17 +      der = Pt.infer_derivs' I (false, Pt.PAxm ("Pure.unconstrainT", prop, SOME [])),
   13.18        tags = [],
   13.19        maxidx = Int.max (maxidx, i),
   13.20        shyps = Sorts.remove_sort S shyps,