src/Pure/Proof/proof_rewrite_rules.ML

       else NONE;
     val equal_intr_axm = ax Proofterm.equal_intr_axm [];
     val equal_elim_axm = ax Proofterm.equal_elim_axm [];
     val symmetric_axm = ax Proofterm.symmetric_axm [propT];
 
-    fun rew' (PThm ({name = "Pure.protectD", ...}, _) % _ %%
-        (PThm ({name = "Pure.protectI", ...}, _) % _ %% prf)) = SOME prf
-      | rew' (PThm ({name = "Pure.conjunctionD1", ...}, _) % _ % _ %%
-        (PThm ({name = "Pure.conjunctionI", ...}, _) % _ % _ %% prf %% _)) = SOME prf
-      | rew' (PThm ({name = "Pure.conjunctionD2", ...}, _) % _ % _ %%
-        (PThm ({name = "Pure.conjunctionI", ...}, _) % _ % _ %% _ %% prf)) = SOME prf
+    fun rew' (PThm ({thm_name = ("Pure.protectD", 0), ...}, _) % _ %%
+        (PThm ({thm_name = ("Pure.protectI", 0), ...}, _) % _ %% prf)) = SOME prf
+      | rew' (PThm ({thm_name = ("Pure.conjunctionD1", 0), ...}, _) % _ % _ %%
+        (PThm ({thm_name = ("Pure.conjunctionI", 0), ...}, _) % _ % _ %% prf %% _)) = SOME prf
+      | rew' (PThm ({thm_name = ("Pure.conjunctionD2", 0), ...}, _) % _ % _ %%
+        (PThm ({thm_name = ("Pure.conjunctionI", 0), ...}, _) % _ % _ %% _ %% 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 ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
         (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.prop", _)) %
           _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %%
-        ((tg as PThm ({name = "Pure.protectI", ...}, _)) % _ %% prf2)) =
+        ((tg as PThm ({thm_name = ("Pure.protectI", 0), ...}, _)) % _ %% prf2)) =
         SOME (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
 
       | rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
         (PAxm ("Pure.symmetric", _, _) % _ % _ %%
           (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.prop", _)) %
              _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1)) %%
-        ((tg as PThm ({name = "Pure.protectI", ...}, _)) % _ %% prf2)) =
+        ((tg as PThm ({thm_name = ("Pure.protectI", 0), ...}, _)) % _ %% prf2)) =
         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", _, _) % _ % _ % _ % _ %%

       (Abst (s, SOME T, fst (insert_refl defs (T :: Ts) prf)), false)
   | insert_refl defs Ts (AbsP (s, t, prf)) =
       (AbsP (s, t, fst (insert_refl defs Ts prf)), false)
   | insert_refl defs Ts prf =
       (case Proofterm.strip_combt prf of
-        (PThm ({name = s, prop, types = SOME Ts, ...}, _), ts) =>
-          if member (op =) defs s then
+        (PThm ({thm_name, prop, types = SOME Ts, ...}, _), ts) =>
+          if member (op =) defs thm_name then
             let
               val vs = vars_of prop;
               val tvars = build_rev (Term.add_tvars prop);
               val (_, rhs) = Logic.dest_equals (Logic.strip_imp_concl prop);
               val rhs' = Term.betapplys (subst_TVars (map fst tvars ~~ Ts)

     val prf' =
       if r then
         let
           val cnames = map (fst o dest_Const o fst) defs';
           val expand = Proofterm.fold_proof_atoms true
-            (fn PThm ({serial, name, prop, ...}, _) =>
-                if member (op =) defnames name orelse
+            (fn PThm ({serial, thm_name, prop, ...}, _) =>
+                if member (op =) defnames thm_name orelse
                   not (exists_Const (member (op =) cnames o #1) prop)
                 then I
-                else Inttab.update (serial, "")
+                else Inttab.update (serial, Thm_Name.empty)
               | _ => I) [prf] Inttab.empty;
         in Proofterm.expand_proof thy (Inttab.lookup expand o #serial) prf end
       else prf;
   in
     rewrite_terms (Pattern.rewrite_term thy defs' [])