src/HOL/Tools/inductive_realizer.ML

     val Tvs = map TVar iTs;
     val (_ $ (_ $ _ $ S)) = Logic.strip_imp_concl (prop_of (hd intrs));
     val (Const (s, _), ts) = strip_comb S;
     val params = map dest_Var ts;
     val tname = space_implode "_" (Sign.base_name s ^ "T" :: vs);
-    fun constr_of_intr intr = (Sign.base_name (Thm.name_of_thm intr),
+    fun constr_of_intr intr = (Sign.base_name (Thm.get_name intr),
       map (Logic.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @
         filter_out (equal Extraction.nullT) (map
           (Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
             NoSyn);
   in (map (fn a => "'" ^ a) vs @ map (fst o fst) iTs, tname, NoSyn,

       | fun_of ts rts args used [] =
           let val xs = rev (rts @ ts)
           in if conclT = Extraction.nullT
             then list_abs_free (map dest_Free xs, HOLogic.unit)
             else list_abs_free (map dest_Free xs, list_comb
-              (Free ("r" ^ Sign.base_name (Thm.name_of_thm intr),
+              (Free ("r" ^ Sign.base_name (Thm.get_name intr),
                 map fastype_of (rev args) ---> conclT), rev args))
           end
 
   in fun_of args' [] (rev args) used (Logic.strip_imp_prems rule') end;
 

       end) (rec_names ~~ concls')
   in if null rlzs then Extraction.nullt else
     let
       val r = foldr1 HOLogic.mk_prod rlzs;
       val x = Free ("x", Extraction.etype_of thy vs [] (hd (prems_of induct)));
-      fun name_of_fn intr = "r" ^ Sign.base_name (Thm.name_of_thm intr);
+      fun name_of_fn intr = "r" ^ Sign.base_name (Thm.get_name intr);
       val r' = list_abs_free (List.mapPartial (fn intr =>
         Option.map (pair (name_of_fn intr)) (AList.lookup (op =) frees (name_of_fn intr))) intrs,
           if length concls = 1 then r $ x else r)
     in
       if length concls = 1 then lambda x r' else r'

           if Extraction.etype_of thy vs [] prem = Extraction.nullT
           then AbsP ("H", SOME rprem, mk_prf rs prems prf)
           else forall_intr_prf (Var (hd rs), AbsP ("H", SOME rprem,
             mk_prf (tl rs) prems prf));
 
-  in (Thm.name_of_thm rule, (vs,
+  in (Thm.get_name rule, (vs,
     if rt = Extraction.nullt then rt else
       foldr (uncurry lambda) rt vs1,
     foldr forall_intr_prf (mk_prf rs prems (Proofterm.proof_combP
       (prf_of rrule, map PBound (length prems - 1 downto 0)))) vs2))
   end;

     (** realizability predicate **)
 
     val (thy3', ind_info) = thy2 |>
       OldInductivePackage.add_inductive_i false true "" false false false
         (map Logic.unvarify rlzsets) (map (fn (rintr, intr) =>
-          ((Sign.base_name (Thm.name_of_thm intr), strip_all
+          ((Sign.base_name (Thm.get_name intr), strip_all
             (Logic.unvarify rintr)), [])) (rintrs ~~ intrs)) [] |>>
       Theory.absolute_path;
     val thy3 = PureThy.hide_thms false
-      (map Thm.name_of_thm (#intrs ind_info)) thy3';
+      (map Thm.get_name (#intrs ind_info)) thy3';
 
     (** realizer for induction rule **)
 
     val Ps = List.mapPartial (fn _ $ M $ P => if set_of M mem rsets then
       SOME (fst (fst (dest_Var (head_of P)))) else NONE)

            rewrite_goals_tac rews,
            REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
              [K (rewrite_goals_tac rews), ObjectLogic.atomize_tac,
               DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
         val (thm', thy') = PureThy.store_thm ((space_implode "_"
-          (Thm.name_of_thm induct :: vs @ Ps @ ["correctness"]), thm), []) thy
+          (Thm.get_name induct :: vs @ Ps @ ["correctness"]), thm), []) thy
       in
         Extraction.add_realizers_i
           [mk_realizer thy' (vs @ Ps) params' ((induct, thm'), r)] thy'
       end;
 

            ALLGOALS (EVERY' [etac Pair_inject, asm_simp_tac HOL_basic_ss]),
            rewrite_goals_tac rews,
            REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_tac THEN'
              DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
         val (thm', thy') = PureThy.store_thm ((space_implode "_"
-          (Thm.name_of_thm elim :: vs @ Ps @ ["correctness"]), thm), []) thy
+          (Thm.get_name elim :: vs @ Ps @ ["correctness"]), thm), []) thy
       in
         Extraction.add_realizers_i
           [mk_realizer thy' (vs @ Ps) params' ((elim, thm'), r)] thy'
       end;