src/HOL/Import/proof_kernel.ML

 val disj2_thm = thm "disjI2"
 
 local
     val th = thm "not_def"
     val thy = theory_of_thm th
-    val pp = Thm.reflexive (cterm_of thy (Const(@{const_name "Trueprop"},HOLogic.boolT-->propT)))
+    val pp = Thm.reflexive (cterm_of thy (Const(@{const_name Trueprop},HOLogic.boolT-->propT)))
 in
 val not_elim_thm = Thm.combination pp th
 end
 
 val not_intro_thm = Thm.symmetric not_elim_thm

         val th2 = beta_eta_thm (Thm.forall_intr cv th1)
         val th3 = th2 COMP (beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME clc] gen_thm))
         val c = prop_of th3
         val vname = fst(dest_Free v)
         val (cold,cnew) = case c of
-                              tpc $ (Const(@{const_name "All"},allT) $ Abs(oldname,ty,body)) =>
+                              tpc $ (Const(@{const_name All},allT) $ Abs(oldname,ty,body)) =>
                               (Abs(oldname,dummyT,Bound 0),Abs(vname,dummyT,Bound 0))
-                            | tpc $ (Const(@{const_name "All"},allT) $ rest) => (tpc,tpc)
+                            | tpc $ (Const(@{const_name All},allT) $ rest) => (tpc,tpc)
                             | _ => raise ERR "mk_GEN" "Unknown conclusion"
         val th4 = Thm.rename_boundvars cold cnew th3
         val res = implies_intr_hyps th4
     in
         res

               | NONE => NONE
         end
 
 fun non_trivial_term_consts t = fold_aterms
   (fn Const (c, _) =>
-      if c = "Trueprop" orelse c = "All" orelse c = "op -->" orelse c = "op &" orelse c = "op ="
+      if c = @{const_name Trueprop} orelse c = @{const_name All}
+        orelse c = @{const_name "op -->"} orelse c = @{const_name "op &"} orelse c = @{const_name "op ="}
       then I else insert (op =) c
     | _ => I) t [];
 
 fun match_consts t (* th *) =
     let
         fun add_consts (Const (c, _), cs) =
             (case c of
-                 "op =" => insert (op =) "==" cs
-               | "op -->" => insert (op =) "==>" cs
-               | "All" => cs
+                 @{const_name "op ="} => insert (op =) "==" cs
+               | @{const_name "op -->"} => insert (op =) "==>" cs
+               | @{const_name All} => cs
                | "all" => cs
-               | "op &" => cs
-               | "Trueprop" => cs
+               | @{const_name "op &"} => cs
+               | @{const_name Trueprop} => cs
                | _ => insert (op =) c cs)
           | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs))
           | add_consts (Abs (_, _, t), cs) = add_consts (t, cs)
           | add_consts (_, cs) = cs
         val t_consts = add_consts(t,[])

         val (info,th) = disamb_thm hth
         val (info',[ex',wit']) = disamb_terms_from info [ex,wit]
         val cwit = cterm_of thy wit'
         val cty = ctyp_of_term cwit
         val a = case ex' of
-                    (Const(@{const_name "Ex"},_) $ a) => a
+                    (Const(@{const_name Ex},_) $ a) => a
                   | _ => raise ERR "EXISTS" "Argument not existential"
         val ca = cterm_of thy a
         val exists_thm' = beta_eta_thm (Drule.instantiate' [SOME cty] [SOME ca,SOME cwit] exists_thm)
         val th1 = beta_eta_thm th
         val th2 = implies_elim_all th1

         val th2 = norm_hyps th2
         val cvty = ctyp_of_term cv
         val c = HOLogic.dest_Trueprop (concl_of th2)
         val cc = cterm_of thy c
         val a = case concl_of th1 of
-                    _ $ (Const(@{const_name "Ex"},_) $ a) => a
+                    _ $ (Const(@{const_name Ex},_) $ a) => a
                   | _ => raise ERR "CHOOSE" "Conclusion not existential"
         val ca = cterm_of (theory_of_thm th1) a
         val choose_thm' = beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME ca,SOME cc] choose_thm)
         val th21 = rearrange thy (HOLogic.mk_Trueprop (a $ v')) th2
         val th22 = strip ((nprems_of th21)-1) (cprems_of th21) th21

         val _ = if_debug pth hth
         val (info,th) = disamb_thm hth
         val (info',tm') = disamb_term_from info tm
         val th = norm_hyps th
         val ct = cterm_of thy tm'
-        val th1 = rearrange thy (HOLogic.mk_Trueprop (Const(@{const_name "Not"},HOLogic.boolT-->HOLogic.boolT) $ tm')) th
+        val th1 = rearrange thy (HOLogic.mk_Trueprop (Const(@{const_name Not},HOLogic.boolT-->HOLogic.boolT) $ tm')) th
         val ccontr_thm' = Drule.instantiate' [] [SOME ct] ccontr_thm
         val res1 = uniq_compose ((nprems_of th1) - 1) th1 1 ccontr_thm'
         val res = HOLThm(rens_of info',res1)
         val _ = message "RESULT:"
         val _ = if_debug pth res

     let
         val _ = message "NOT_INTRO:"
         val _ = if_debug pth hth
         val th1 = implies_elim_all (beta_eta_thm th)
         val a = case concl_of th1 of
-                    _ $ (Const(@{const_name "op -->"},_) $ a $ Const(@{const_name "False"},_)) => a
+                    _ $ (Const(@{const_name "op -->"},_) $ a $ Const(@{const_name False},_)) => a
                   | _ => raise ERR "NOT_INTRO" "Conclusion of bad form"
         val ca = cterm_of thy a
         val th2 = Thm.equal_elim (Drule.instantiate' [] [SOME ca] not_intro_thm) th1
         val res = HOLThm(rens,implies_intr_hyps th2)
         val _ = message "RESULT:"

     let
         val _ = message "NOT_INTRO:"
         val _ = if_debug pth hth
         val th1 = implies_elim_all (beta_eta_thm th)
         val a = case concl_of th1 of
-                    _ $ (Const(@{const_name "Not"},_) $ a) => a
+                    _ $ (Const(@{const_name Not},_) $ a) => a
                   | _ => raise ERR "NOT_ELIM" "Conclusion of bad form"
         val ca = cterm_of thy a
         val th2 = Thm.equal_elim (Drule.instantiate' [] [SOME ca] not_elim_thm) th1
         val res = HOLThm(rens,implies_intr_hyps th2)
         val _ = message "RESULT:"

                                        val (dT,rT) = dom_rng (type_of body)
                                    in
                                        ("x",dT,body $ Bound 0)
                                    end
                                    handle TYPE _ => raise ERR "new_specification" "not an abstraction type"
-                               fun dest_exists (Const(@{const_name "Ex"},_) $ abody) =
+                               fun dest_exists (Const(@{const_name Ex},_) $ abody) =
                                    dest_eta_abs abody
                                  | dest_exists tm =
                                    raise ERR "new_specification" "Bad existential formula"
 
                                val (consts,_) = Library.foldl (fn ((cs,ex),cname) =>

             val _ = if_debug pth hth
             val _ = warning ("Introducing type " ^ tycname)
             val (HOLThm(rens,td_th)) = norm_hthm thy hth
             val th2 = beta_eta_thm (td_th RS ex_imp_nonempty)
             val c = case concl_of th2 of
-                        _ $ (Const(@{const_name "Ex"},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
+                        _ $ (Const(@{const_name Ex},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
                       | _ => raise ERR "new_type_definition" "Bad type definition theorem"
             val tfrees = OldTerm.term_tfrees c
             val tnames = map fst tfrees
             val tsyn = mk_syn thy tycname
             val typ = (tycname,tnames,tsyn)

             val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
 
             val rew = rewrite_hol4_term (concl_of td_th) thy4
             val th  = Thm.equal_elim rew (Thm.transfer thy4 td_th)
             val c   = case HOLogic.dest_Trueprop (prop_of th) of
-                          Const(@{const_name "Ex"},exT) $ P =>
+                          Const(@{const_name Ex},exT) $ P =>
                           let
                               val PT = domain_type exT
                           in
                               Const (@{const_name Collect},PT-->HOLogic.mk_setT (domain_type PT)) $ P
                           end

                 Drule.instantiate' [SOME (ctyp_of thy tT)]
                                    [SOME (cterm_of thy P),
                                     SOME (cterm_of thy t)] light_nonempty
             val th2 = beta_eta_thm (td_th RS (beta_eta_thm light_nonempty'))
             val c = case concl_of th2 of
-                        _ $ (Const(@{const_name "Ex"},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
+                        _ $ (Const(@{const_name Ex},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
                       | _ => raise ERR "type_introduction" "Bad type definition theorem"
             val tfrees = OldTerm.term_tfrees c
             val tnames = sort_strings (map fst tfrees)
             val tsyn = mk_syn thy tycname
             val typ = (tycname,tnames,tsyn)