src/Pure/Proof/proof_rewrite_rules.ML

         SOME (tg %> B %% (equal_elim_axm %> A %> B %%
           (symmetric_axm % ?? B % ?? A %% prf1) %% prf2))
 
       | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
         (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
-          (PAxm ("Pure.combination", _, _) % SOME (Const ("==>", _)) % _ % _ % _ %%
+          (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.imp", _)) % _ % _ % _ %%
              (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2)) =
         let
           val _ $ A $ C = Envir.beta_norm X;
           val _ $ B $ D = Envir.beta_norm Y
         in SOME (AbsP ("H1", ?? X, AbsP ("H2", ?? B,

         end
 
       | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
         (PAxm ("Pure.symmetric", _, _) % _ % _ %%
           (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
-            (PAxm ("Pure.combination", _, _) % SOME (Const ("==>", _)) % _ % _ % _ %%
+            (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.imp", _)) % _ % _ % _ %%
                (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2))) =
         let
           val _ $ A $ C = Envir.beta_norm Y;
           val _ $ B $ D = Envir.beta_norm X
         in SOME (AbsP ("H1", ?? X, AbsP ("H2", ?? A,

               (PBound 1 %%
                 (equal_elim_axm %> A %> B %% Proofterm.incr_pboundvars 2 0 prf1 %% PBound 0)))))
         end
 
       | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
-        (PAxm ("Pure.combination", _, _) % SOME (Const ("all", _)) % _ % _ % _ %%
+        (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.all", _)) % _ % _ % _ %%
           (PAxm ("Pure.reflexive", _, _) % _) %%
             (PAxm ("Pure.abstract_rule", _, _) % _ % _ %% prf))) =
         let
           val Const (_, T) $ P = Envir.beta_norm X;
           val _ $ Q = Envir.beta_norm Y;

               (Proofterm.incr_pboundvars 1 1 prf %> Bound 0) %% (PBound 0 %> Bound 0))))
         end
 
       | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
         (PAxm ("Pure.symmetric", _, _) % _ % _ %%        
-          (PAxm ("Pure.combination", _, _) % SOME (Const ("all", _)) % _ % _ % _ %%
+          (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.all", _)) % _ % _ % _ %%
             (PAxm ("Pure.reflexive", _, _) % _) %%
               (PAxm ("Pure.abstract_rule", _, _) % _ % _ %% prf)))) =
         let
           val Const (_, T) $ P = Envir.beta_norm X;
           val _ $ Q = Envir.beta_norm Y;

         (PAxm ("Pure.symmetric", _, _) % _ % _ %% prf)) = SOME prf
 
       | 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.combination", _, _) % SOME (Const ("Pure.eq", _)) % _ % _ % _ %%
               (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 ("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.combination", _, _) % SOME (Const ("Pure.eq", _)) % _ % _ % _ %%
                 (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 ("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.combination", _, _) % SOME (Const ("Pure.eq", _)) % _ % _ % _ %%
                 (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 ("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.combination", _, _) % SOME (Const ("Pure.eq", _)) % _ % _ % _ %%
                   (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 ("Pure.combination", _, _) %
-        SOME ((eq as Const ("==", T)) $ t) % _ % _ % _) %%
+        SOME ((eq as Const ("Pure.eq", T)) $ t) % _ % _ % _) %%
           (PAxm ("Pure.reflexive", _, _) % _)) =
         let val (U, V) = (case T of
           Type (_, [U, V]) => (U, V) | _ => (dummyT, dummyT))
         in SOME (prf %% (ax Proofterm.combination_axm [U, V] %> eq % ?? eq % ?? t % ?? t %%
           (ax Proofterm.reflexive_axm [T] % ?? eq) %% (ax Proofterm.reflexive_axm [U] % ?? t)))

     val params = Logic.strip_params Q;
     val Hs = Logic.strip_assums_hyp P;
     val Hs' = Logic.strip_assums_hyp Q;
     val k = length Hs;
     val l = length params;
-    fun mk_prf i j Hs Hs' (Const ("all", _) $ Abs (_, _, P)) prf =
+    fun mk_prf i j Hs Hs' (Const ("Pure.all", _) $ Abs (_, _, P)) prf =
           mk_prf i (j - 1) Hs Hs' P (prf %> Bound j)
-      | mk_prf i j (H :: Hs) (H' :: Hs') (Const ("==>", _) $ _ $ P) prf =
+      | mk_prf i j (H :: Hs) (H' :: Hs') (Const ("Pure.imp", _) $ _ $ P) prf =
           mk_prf (i - 1) j Hs Hs' P (prf %% un_hhf_proof H' H (PBound i))
       | mk_prf _ _ _ _ _ prf = prf
   in
     prf |> Proofterm.incr_pboundvars k l |> mk_prf (k - 1) (l - 1) Hs Hs' P |>
     fold_rev (fn P => fn prf => AbsP ("H", SOME P, prf)) Hs' |>

     val params = Logic.strip_params Q;
     val Hs = Logic.strip_assums_hyp P;
     val Hs' = Logic.strip_assums_hyp Q;
     val k = length Hs;
     val l = length params;
-    fun mk_prf (Const ("all", _) $ Abs (s, T, P)) prf =
+    fun mk_prf (Const ("Pure.all", _) $ Abs (s, T, P)) prf =
           Abst (s, SOME T, mk_prf P prf)
-      | mk_prf (Const ("==>", _) $ P $ Q) prf =
+      | mk_prf (Const ("Pure.imp", _) $ P $ Q) prf =
           AbsP ("H", SOME P, mk_prf Q prf)
       | mk_prf _ prf = prf
   in
     prf |> Proofterm.incr_pboundvars k l |>
     fold (fn i => fn prf => prf %> Bound i) (l - 1 downto 0) |>