use antiquotations for remaining unqualified constants in HOL
authorhaftmann
Thu Aug 19 11:02:14 2010 +0200 (2010-08-19)
changeset 38549d0385f2764d8
parent 38548 dea0d2cca822
child 38550 925c4d7b291e
use antiquotations for remaining unqualified constants in HOL
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/Cooper.thy
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Decision_Procs/cooper_tac.ML
src/HOL/Decision_Procs/ferrack_tac.ML
src/HOL/Decision_Procs/ferrante_rackoff.ML
src/HOL/Decision_Procs/langford.ML
src/HOL/Decision_Procs/mir_tac.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Import/shuffler.ML
src/HOL/Library/Eval_Witness.thy
src/HOL/Library/positivstellensatz.ML
src/HOL/Library/reflection.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Nominal/nominal_thmdecls.ML
src/HOL/Prolog/prolog.ML
src/HOL/Statespace/distinct_tree_prover.ML
src/HOL/Statespace/state_fun.ML
src/HOL/Statespace/state_space.ML
src/HOL/TLA/Intensional.thy
src/HOL/Tools/Function/function_core.ML
src/HOL/Tools/Function/termination.ML
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/Sledgehammer/metis_tactics.ML
src/HOL/Tools/TFL/post.ML
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/TFL/usyntax.ML
src/HOL/Tools/choice_specification.ML
src/HOL/Tools/cnf_funcs.ML
src/HOL/Tools/groebner.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/numeral_simprocs.ML
src/HOL/Tools/prop_logic.ML
src/HOL/Tools/quickcheck_generators.ML
src/HOL/Tools/sat_funcs.ML
src/HOL/ex/SVC_Oracle.thy
src/HOL/ex/svc_funcs.ML
src/HOLCF/Tools/Domain/domain_library.ML
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Thu Aug 19 10:27:12 2010 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Aug 19 11:02:14 2010 +0200
     1.3 @@ -3301,11 +3301,11 @@
     1.4  ML {*
     1.5    fun reorder_bounds_tac prems i =
     1.6      let
     1.7 -      fun variable_of_bound (Const ("Trueprop", _) $
     1.8 +      fun variable_of_bound (Const (@{const_name "Trueprop"}, _) $
     1.9                               (Const (@{const_name Set.member}, _) $
    1.10                                Free (name, _) $ _)) = name
    1.11 -        | variable_of_bound (Const ("Trueprop", _) $
    1.12 -                             (Const ("op =", _) $
    1.13 +        | variable_of_bound (Const (@{const_name "Trueprop"}, _) $
    1.14 +                             (Const (@{const_name "op ="}, _) $
    1.15                                Free (name, _) $ _)) = name
    1.16          | variable_of_bound t = raise TERM ("variable_of_bound", [t])
    1.17  
     2.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Thu Aug 19 10:27:12 2010 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Thu Aug 19 11:02:14 2010 +0200
     2.3 @@ -1960,12 +1960,12 @@
     2.4        @{code Imp} (fm_of_term ps vs t1, fm_of_term ps vs t2)
     2.5    | fm_of_term ps vs (@{term "Not"} $ t') =
     2.6        @{code NOT} (fm_of_term ps vs t')
     2.7 -  | fm_of_term ps vs (Const ("Ex", _) $ Abs (xn, xT, p)) =
     2.8 +  | fm_of_term ps vs (Const (@{const_name "Ex"}, _) $ Abs (xn, xT, p)) =
     2.9        let
    2.10          val (xn', p') = variant_abs (xn, xT, p);
    2.11          val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
    2.12        in @{code E} (fm_of_term ps vs' p) end
    2.13 -  | fm_of_term ps vs (Const ("All", _) $ Abs (xn, xT, p)) =
    2.14 +  | fm_of_term ps vs (Const (@{const_name "All"}, _) $ Abs (xn, xT, p)) =
    2.15        let
    2.16          val (xn', p') = variant_abs (xn, xT, p);
    2.17          val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
     3.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Thu Aug 19 10:27:12 2010 +0200
     3.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Thu Aug 19 11:02:14 2010 +0200
     3.3 @@ -519,9 +519,9 @@
     3.4    val [lt, le] = map (Morphism.term phi) [@{term "op \<sqsubset>"}, @{term "op \<sqsubseteq>"}]
     3.5    fun h x t =
     3.6     case term_of t of
     3.7 -     Const("op =", _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
     3.8 +     Const(@{const_name "op ="}, _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
     3.9                              else Ferrante_Rackoff_Data.Nox
    3.10 -   | @{term "Not"}$(Const("op =", _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
    3.11 +   | @{term "Not"}$(Const(@{const_name "op ="}, _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
    3.12                              else Ferrante_Rackoff_Data.Nox
    3.13     | b$y$z => if Term.could_unify (b, lt) then
    3.14                   if term_of x aconv y then Ferrante_Rackoff_Data.Lt
    3.15 @@ -771,7 +771,7 @@
    3.16        in rth end
    3.17      | _ => Thm.reflexive ct)
    3.18  
    3.19 -|  Const("op =",_)$_$Const(@{const_name Groups.zero},_) =>
    3.20 +|  Const(@{const_name "op ="},_)$_$Const(@{const_name Groups.zero},_) =>
    3.21     (case whatis x (Thm.dest_arg1 ct) of
    3.22      ("c*x+t",[c,t]) =>
    3.23         let
    3.24 @@ -835,7 +835,7 @@
    3.25         val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    3.26     in rth end
    3.27  
    3.28 -| Const("op =",_)$a$b =>
    3.29 +| Const(@{const_name "op ="},_)$a$b =>
    3.30     let val (ca,cb) = Thm.dest_binop ct
    3.31         val T = ctyp_of_term ca
    3.32         val th = instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0
    3.33 @@ -844,7 +844,7 @@
    3.34                (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
    3.35         val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    3.36     in rth end
    3.37 -| @{term "Not"} $(Const("op =",_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
    3.38 +| @{term "Not"} $(Const(@{const_name "op ="},_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
    3.39  | _ => Thm.reflexive ct
    3.40  end;
    3.41  
    3.42 @@ -852,9 +852,9 @@
    3.43   let
    3.44    fun h x t =
    3.45     case term_of t of
    3.46 -     Const("op =", _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
    3.47 +     Const(@{const_name "op ="}, _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
    3.48                              else Ferrante_Rackoff_Data.Nox
    3.49 -   | @{term "Not"}$(Const("op =", _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
    3.50 +   | @{term "Not"}$(Const(@{const_name "op ="}, _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
    3.51                              else Ferrante_Rackoff_Data.Nox
    3.52     | Const(@{const_name Orderings.less},_)$y$z =>
    3.53         if term_of x aconv y then Ferrante_Rackoff_Data.Lt
     4.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Thu Aug 19 10:27:12 2010 +0200
     4.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Thu Aug 19 11:02:14 2010 +0200
     4.3 @@ -2000,9 +2000,9 @@
     4.4    | fm_of_term vs (@{term "op |"} $ t1 $ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
     4.5    | fm_of_term vs (@{term "op -->"} $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
     4.6    | fm_of_term vs (@{term "Not"} $ t') = @{code NOT} (fm_of_term vs t')
     4.7 -  | fm_of_term vs (Const ("Ex", _) $ Abs (xn, xT, p)) =
     4.8 +  | fm_of_term vs (Const (@{const_name "Ex"}, _) $ Abs (xn, xT, p)) =
     4.9        @{code E} (fm_of_term (("", dummyT) :: vs) p)
    4.10 -  | fm_of_term vs (Const ("All", _) $ Abs (xn, xT, p)) =
    4.11 +  | fm_of_term vs (Const (@{const_name "All"}, _) $ Abs (xn, xT, p)) =
    4.12        @{code A} (fm_of_term (("", dummyT) ::  vs) p)
    4.13    | fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t);
    4.14  
     5.1 --- a/src/HOL/Decision_Procs/MIR.thy	Thu Aug 19 10:27:12 2010 +0200
     5.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Thu Aug 19 11:02:14 2010 +0200
     5.3 @@ -5845,9 +5845,9 @@
     5.4        @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
     5.5    | fm_of_term vs (@{term "Not"} $ t') =
     5.6        @{code NOT} (fm_of_term vs t')
     5.7 -  | fm_of_term vs (Const ("Ex", _) $ Abs (xn, xT, p)) =
     5.8 +  | fm_of_term vs (Const (@{const_name "Ex"}, _) $ Abs (xn, xT, p)) =
     5.9        @{code E} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p)
    5.10 -  | fm_of_term vs (Const ("All", _) $ Abs (xn, xT, p)) =
    5.11 +  | fm_of_term vs (Const (@{const_name "All"}, _) $ Abs (xn, xT, p)) =
    5.12        @{code A} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p)
    5.13    | fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t);
    5.14  
     6.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Aug 19 10:27:12 2010 +0200
     6.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Aug 19 11:02:14 2010 +0200
     6.3 @@ -2960,7 +2960,7 @@
     6.4  val ifft = @{term "op = :: bool => _"}
     6.5  fun llt rT = Const(@{const_name Orderings.less},rrT rT);
     6.6  fun lle rT = Const(@{const_name Orderings.less},rrT rT);
     6.7 -fun eqt rT = Const("op =",rrT rT);
     6.8 +fun eqt rT = Const(@{const_name "op ="},rrT rT);
     6.9  fun rz rT = Const(@{const_name Groups.zero},rT);
    6.10  
    6.11  fun dest_nat t = case t of
    6.12 @@ -3015,26 +3015,26 @@
    6.13  
    6.14  fun fm_of_term m m' fm = 
    6.15   case fm of
    6.16 -    Const("True",_) => @{code T}
    6.17 -  | Const("False",_) => @{code F}
    6.18 -  | Const("Not",_)$p => @{code NOT} (fm_of_term m m' p)
    6.19 -  | Const("op &",_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
    6.20 -  | Const("op |",_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
    6.21 -  | Const("op -->",_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
    6.22 -  | Const("op =",ty)$p$q => 
    6.23 +    Const(@{const_name "True"},_) => @{code T}
    6.24 +  | Const(@{const_name "False"},_) => @{code F}
    6.25 +  | Const(@{const_name "Not"},_)$p => @{code NOT} (fm_of_term m m' p)
    6.26 +  | Const(@{const_name "op &"},_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
    6.27 +  | Const(@{const_name "op |"},_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
    6.28 +  | Const(@{const_name "op -->"},_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
    6.29 +  | Const(@{const_name "op ="},ty)$p$q => 
    6.30         if domain_type ty = bT then @{code Iff} (fm_of_term m m' p, fm_of_term m m' q)
    6.31         else @{code Eq} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
    6.32    | Const(@{const_name Orderings.less},_)$p$q => 
    6.33          @{code Lt} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
    6.34    | Const(@{const_name Orderings.less_eq},_)$p$q => 
    6.35          @{code Le} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
    6.36 -  | Const("Ex",_)$Abs(xn,xT,p) => 
    6.37 +  | Const(@{const_name "Ex"},_)$Abs(xn,xT,p) => 
    6.38       let val (xn', p') =  variant_abs (xn,xT,p)
    6.39           val x = Free(xn',xT)
    6.40           fun incr i = i + 1
    6.41           val m0 = (x,0):: (map (apsnd incr) m)
    6.42        in @{code E} (fm_of_term m0 m' p') end
    6.43 -  | Const("All",_)$Abs(xn,xT,p) => 
    6.44 +  | Const(@{const_name "All"},_)$Abs(xn,xT,p) => 
    6.45       let val (xn', p') =  variant_abs (xn,xT,p)
    6.46           val x = Free(xn',xT)
    6.47           fun incr i = i + 1
    6.48 @@ -3045,8 +3045,8 @@
    6.49  
    6.50  fun term_of_fm T m m' t = 
    6.51    case t of
    6.52 -    @{code T} => Const("True",bT)
    6.53 -  | @{code F} => Const("False",bT)
    6.54 +    @{code T} => Const(@{const_name "True"},bT)
    6.55 +  | @{code F} => Const(@{const_name "False"},bT)
    6.56    | @{code NOT} p => nott $ (term_of_fm T m m' p)
    6.57    | @{code And} (p,q) => conjt $ (term_of_fm T m m' p) $ (term_of_fm T m m' q)
    6.58    | @{code Or} (p,q) => disjt $ (term_of_fm T m m' p) $ (term_of_fm T m m' q)
     7.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Thu Aug 19 10:27:12 2010 +0200
     7.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Thu Aug 19 11:02:14 2010 +0200
     7.3 @@ -110,7 +110,7 @@
     7.4      fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
     7.5      (* The result of the quantifier elimination *)
     7.6      val (th, tac) = case (prop_of pre_thm) of
     7.7 -        Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
     7.8 +        Const ("==>", _) $ (Const (@{const_name "Trueprop"}, _) $ t1) $ _ =>
     7.9      let val pth = linzqe_oracle (cterm_of thy (Pattern.eta_long [] t1))
    7.10      in
    7.11            ((pth RS iffD2) RS pre_thm,
     8.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML	Thu Aug 19 10:27:12 2010 +0200
     8.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Thu Aug 19 11:02:14 2010 +0200
     8.3 @@ -91,7 +91,7 @@
     8.4      fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
     8.5      (* The result of the quantifier elimination *)
     8.6      val (th, tac) = case prop_of pre_thm of
     8.7 -        Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
     8.8 +        Const ("==>", _) $ (Const (@{const_name "Trueprop"}, _) $ t1) $ _ =>
     8.9      let val pth = linr_oracle (ctxt, Pattern.eta_long [] t1)
    8.10      in 
    8.11            (trace_msg ("calling procedure with term:\n" ^
     9.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Aug 19 10:27:12 2010 +0200
     9.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Aug 19 11:02:14 2010 +0200
     9.3 @@ -33,12 +33,12 @@
     9.4               {isolate_conv = icv, whatis = wi, simpset = simpset}):entry) =
     9.5  let
     9.6   fun uset (vars as (x::vs)) p = case term_of p of
     9.7 -   Const("op &", _)$ _ $ _ =>
     9.8 +   Const(@{const_name "op &"}, _)$ _ $ _ =>
     9.9       let
    9.10         val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
    9.11         val (lS,lth) = uset vars l  val (rS, rth) = uset vars r
    9.12       in (lS@rS, Drule.binop_cong_rule b lth rth) end
    9.13 - |  Const("op |", _)$ _ $ _ =>
    9.14 + |  Const(@{const_name "op |"}, _)$ _ $ _ =>
    9.15       let
    9.16         val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
    9.17         val (lS,lth) = uset vars l  val (rS, rth) = uset vars r
    9.18 @@ -77,7 +77,7 @@
    9.19   fun main vs p =
    9.20    let
    9.21     val ((xn,ce),(x,fm)) = (case term_of p of
    9.22 -                   Const("Ex",_)$Abs(xn,xT,_) =>
    9.23 +                   Const(@{const_name "Ex"},_)$Abs(xn,xT,_) =>
    9.24                          Thm.dest_comb p ||> Thm.dest_abs (SOME xn) |>> pair xn
    9.25                   | _ => raise CTERM ("main QE only treats existential quantifiers!", [p]))
    9.26     val cT = ctyp_of_term x
    9.27 @@ -122,12 +122,12 @@
    9.28  
    9.29     fun decomp_mpinf fm =
    9.30       case term_of fm of
    9.31 -       Const("op &",_)$_$_ =>
    9.32 +       Const(@{const_name "op &"},_)$_$_ =>
    9.33          let val (p,q) = Thm.dest_binop fm
    9.34          in ([p,q], myfwd (minf_conj,pinf_conj, nmi_conj, npi_conj,ld_conj)
    9.35                           (Thm.cabs x p) (Thm.cabs x q))
    9.36          end
    9.37 -     | Const("op |",_)$_$_ =>
    9.38 +     | Const(@{const_name "op |"},_)$_$_ =>
    9.39          let val (p,q) = Thm.dest_binop fm
    9.40          in ([p,q],myfwd (minf_disj, pinf_disj, nmi_disj, npi_disj,ld_disj)
    9.41                           (Thm.cabs x p) (Thm.cabs x q))
    9.42 @@ -175,19 +175,19 @@
    9.43   let
    9.44    fun h bounds tm =
    9.45     (case term_of tm of
    9.46 -     Const ("op =", T) $ _ $ _ =>
    9.47 +     Const (@{const_name "op ="}, T) $ _ $ _ =>
    9.48         if domain_type T = HOLogic.boolT then find_args bounds tm
    9.49         else Thm.dest_fun2 tm
    9.50 -   | Const ("Not", _) $ _ => h bounds (Thm.dest_arg tm)
    9.51 -   | Const ("All", _) $ _ => find_body bounds (Thm.dest_arg tm)
    9.52 -   | Const ("Ex", _) $ _ => find_body bounds (Thm.dest_arg tm)
    9.53 -   | Const ("op &", _) $ _ $ _ => find_args bounds tm
    9.54 -   | Const ("op |", _) $ _ $ _ => find_args bounds tm
    9.55 -   | Const ("op -->", _) $ _ $ _ => find_args bounds tm
    9.56 +   | Const (@{const_name "Not"}, _) $ _ => h bounds (Thm.dest_arg tm)
    9.57 +   | Const (@{const_name "All"}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    9.58 +   | Const (@{const_name "Ex"}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    9.59 +   | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
    9.60 +   | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
    9.61 +   | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
    9.62     | Const ("==>", _) $ _ $ _ => find_args bounds tm
    9.63     | Const ("==", _) $ _ $ _ => find_args bounds tm
    9.64     | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
    9.65 -   | Const ("Trueprop", _) $ _ => h bounds (Thm.dest_arg tm)
    9.66 +   | Const (@{const_name "Trueprop"}, _) $ _ => h bounds (Thm.dest_arg tm)
    9.67     | _ => Thm.dest_fun2 tm)
    9.68    and find_args bounds tm =
    9.69             (h bounds (Thm.dest_arg tm) handle CTERM _ => Thm.dest_arg1 tm)
    10.1 --- a/src/HOL/Decision_Procs/langford.ML	Thu Aug 19 10:27:12 2010 +0200
    10.2 +++ b/src/HOL/Decision_Procs/langford.ML	Thu Aug 19 11:02:14 2010 +0200
    10.3 @@ -30,7 +30,7 @@
    10.4  
    10.5  fun basic_dloqe ctxt stupid dlo_qeth dlo_qeth_nolb dlo_qeth_noub gather ep = 
    10.6   case term_of ep of 
    10.7 -  Const("Ex",_)$_ => 
    10.8 +  Const(@{const_name "Ex"},_)$_ => 
    10.9     let 
   10.10       val p = Thm.dest_arg ep
   10.11       val ths = simplify (HOL_basic_ss addsimps gather) (instantiate' [] [SOME p] stupid)
   10.12 @@ -116,13 +116,13 @@
   10.13  fun contains x ct = member (op aconv) (OldTerm.term_frees (term_of ct)) (term_of x);
   10.14  
   10.15  fun is_eqx x eq = case term_of eq of
   10.16 -   Const("op =",_)$l$r => l aconv term_of x orelse r aconv term_of x
   10.17 +   Const(@{const_name "op ="},_)$l$r => l aconv term_of x orelse r aconv term_of x
   10.18   | _ => false ;
   10.19  
   10.20  local 
   10.21  fun proc ct = 
   10.22   case term_of ct of
   10.23 -  Const("Ex",_)$Abs (xn,_,_) => 
   10.24 +  Const(@{const_name "Ex"},_)$Abs (xn,_,_) => 
   10.25     let 
   10.26      val e = Thm.dest_fun ct
   10.27      val (x,p) = Thm.dest_abs (SOME xn) (Thm.dest_arg ct)
   10.28 @@ -176,19 +176,19 @@
   10.29   let
   10.30    fun h bounds tm =
   10.31     (case term_of tm of
   10.32 -     Const ("op =", T) $ _ $ _ =>
   10.33 +     Const (@{const_name "op ="}, T) $ _ $ _ =>
   10.34         if domain_type T = HOLogic.boolT then find_args bounds tm
   10.35         else Thm.dest_fun2 tm
   10.36 -   | Const ("Not", _) $ _ => h bounds (Thm.dest_arg tm)
   10.37 -   | Const ("All", _) $ _ => find_body bounds (Thm.dest_arg tm)
   10.38 +   | Const (@{const_name "Not"}, _) $ _ => h bounds (Thm.dest_arg tm)
   10.39 +   | Const (@{const_name "All"}, _) $ _ => find_body bounds (Thm.dest_arg tm)
   10.40     | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
   10.41 -   | Const ("Ex", _) $ _ => find_body bounds (Thm.dest_arg tm)
   10.42 -   | Const ("op &", _) $ _ $ _ => find_args bounds tm
   10.43 -   | Const ("op |", _) $ _ $ _ => find_args bounds tm
   10.44 -   | Const ("op -->", _) $ _ $ _ => find_args bounds tm
   10.45 +   | Const (@{const_name "Ex"}, _) $ _ => find_body bounds (Thm.dest_arg tm)
   10.46 +   | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
   10.47 +   | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
   10.48 +   | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
   10.49     | Const ("==>", _) $ _ $ _ => find_args bounds tm
   10.50     | Const ("==", _) $ _ $ _ => find_args bounds tm
   10.51 -   | Const ("Trueprop", _) $ _ => h bounds (Thm.dest_arg tm)
   10.52 +   | Const (@{const_name "Trueprop"}, _) $ _ => h bounds (Thm.dest_arg tm)
   10.53     | _ => Thm.dest_fun2 tm)
   10.54    and find_args bounds tm =
   10.55      (h bounds (Thm.dest_arg tm) handle CTERM _ => h bounds (Thm.dest_arg1 tm))
    11.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Thu Aug 19 10:27:12 2010 +0200
    11.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Thu Aug 19 11:02:14 2010 +0200
    11.3 @@ -132,7 +132,7 @@
    11.4      fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
    11.5      (* The result of the quantifier elimination *)
    11.6      val (th, tac) = case (prop_of pre_thm) of
    11.7 -        Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
    11.8 +        Const ("==>", _) $ (Const (@{const_name "Trueprop"}, _) $ t1) $ _ =>
    11.9      let val pth =
   11.10            (* If quick_and_dirty then run without proof generation as oracle*)
   11.11               if !quick_and_dirty
    12.1 --- a/src/HOL/Import/proof_kernel.ML	Thu Aug 19 10:27:12 2010 +0200
    12.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu Aug 19 11:02:14 2010 +0200
    12.3 @@ -1007,7 +1007,7 @@
    12.4  local
    12.5      val th = thm "not_def"
    12.6      val thy = theory_of_thm th
    12.7 -    val pp = Thm.reflexive (cterm_of thy (Const("Trueprop",boolT-->propT)))
    12.8 +    val pp = Thm.reflexive (cterm_of thy (Const(@{const_name "Trueprop"},boolT-->propT)))
    12.9  in
   12.10  val not_elim_thm = Thm.combination pp th
   12.11  end
   12.12 @@ -1053,9 +1053,9 @@
   12.13          val c = prop_of th3
   12.14          val vname = fst(dest_Free v)
   12.15          val (cold,cnew) = case c of
   12.16 -                              tpc $ (Const("All",allT) $ Abs(oldname,ty,body)) =>
   12.17 +                              tpc $ (Const(@{const_name "All"},allT) $ Abs(oldname,ty,body)) =>
   12.18                                (Abs(oldname,dummyT,Bound 0),Abs(vname,dummyT,Bound 0))
   12.19 -                            | tpc $ (Const("All",allT) $ rest) => (tpc,tpc)
   12.20 +                            | tpc $ (Const(@{const_name "All"},allT) $ rest) => (tpc,tpc)
   12.21                              | _ => raise ERR "mk_GEN" "Unknown conclusion"
   12.22          val th4 = Thm.rename_boundvars cold cnew th3
   12.23          val res = implies_intr_hyps th4
   12.24 @@ -1476,10 +1476,10 @@
   12.25  fun mk_COMB th1 th2 thy =
   12.26      let
   12.27          val (f,g) = case concl_of th1 of
   12.28 -                        _ $ (Const("op =",_) $ f $ g) => (f,g)
   12.29 +                        _ $ (Const(@{const_name "op ="},_) $ f $ g) => (f,g)
   12.30                        | _ => raise ERR "mk_COMB" "First theorem not an equality"
   12.31          val (x,y) = case concl_of th2 of
   12.32 -                        _ $ (Const("op =",_) $ x $ y) => (x,y)
   12.33 +                        _ $ (Const(@{const_name "op ="},_) $ x $ y) => (x,y)
   12.34                        | _ => raise ERR "mk_COMB" "Second theorem not an equality"
   12.35          val fty = type_of f
   12.36          val (fd,fr) = dom_rng fty
   12.37 @@ -1521,7 +1521,7 @@
   12.38          val th1 = norm_hyps th1
   12.39          val th2 = norm_hyps th2
   12.40          val (l,r) = case concl_of th of
   12.41 -                        _ $ (Const("op |",_) $ l $ r) => (l,r)
   12.42 +                        _ $ (Const(@{const_name "op |"},_) $ l $ r) => (l,r)
   12.43                        | _ => raise ERR "DISJ_CASES" "Conclusion not a disjunction"
   12.44          val th1' = rearrange thy (HOLogic.mk_Trueprop l) th1
   12.45          val th2' = rearrange thy (HOLogic.mk_Trueprop r) th2
   12.46 @@ -1654,7 +1654,7 @@
   12.47          val cwit = cterm_of thy wit'
   12.48          val cty = ctyp_of_term cwit
   12.49          val a = case ex' of
   12.50 -                    (Const("Ex",_) $ a) => a
   12.51 +                    (Const(@{const_name "Ex"},_) $ a) => a
   12.52                    | _ => raise ERR "EXISTS" "Argument not existential"
   12.53          val ca = cterm_of thy a
   12.54          val exists_thm' = beta_eta_thm (Drule.instantiate' [SOME cty] [SOME ca,SOME cwit] exists_thm)
   12.55 @@ -1687,7 +1687,7 @@
   12.56          val c = HOLogic.dest_Trueprop (concl_of th2)
   12.57          val cc = cterm_of thy c
   12.58          val a = case concl_of th1 of
   12.59 -                    _ $ (Const("Ex",_) $ a) => a
   12.60 +                    _ $ (Const(@{const_name "Ex"},_) $ a) => a
   12.61                    | _ => raise ERR "CHOOSE" "Conclusion not existential"
   12.62          val ca = cterm_of (theory_of_thm th1) a
   12.63          val choose_thm' = beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME ca,SOME cc] choose_thm)
   12.64 @@ -1773,7 +1773,7 @@
   12.65          val (info',tm') = disamb_term_from info tm
   12.66          val th = norm_hyps th
   12.67          val ct = cterm_of thy tm'
   12.68 -        val th1 = rearrange thy (HOLogic.mk_Trueprop (Const("Not",boolT-->boolT) $ tm')) th
   12.69 +        val th1 = rearrange thy (HOLogic.mk_Trueprop (Const(@{const_name "Not"},boolT-->boolT) $ tm')) th
   12.70          val ccontr_thm' = Drule.instantiate' [] [SOME ct] ccontr_thm
   12.71          val res1 = uniq_compose ((nprems_of th1) - 1) th1 1 ccontr_thm'
   12.72          val res = HOLThm(rens_of info',res1)
   12.73 @@ -1788,7 +1788,7 @@
   12.74          val cv = cterm_of thy v
   12.75          val th1 = implies_elim_all (beta_eta_thm th)
   12.76          val (f,g) = case concl_of th1 of
   12.77 -                        _ $ (Const("op =",_) $ f $ g) => (Term.lambda v f,Term.lambda v g)
   12.78 +                        _ $ (Const(@{const_name "op ="},_) $ f $ g) => (Term.lambda v f,Term.lambda v g)
   12.79                        | _ => raise ERR "mk_ABS" "Bad conclusion"
   12.80          val (fd,fr) = dom_rng (type_of f)
   12.81          val abs_thm' = Drule.instantiate' [SOME (ctyp_of thy fd), SOME (ctyp_of thy fr)] [SOME (cterm_of thy f), SOME (cterm_of thy g)] abs_thm
   12.82 @@ -1860,7 +1860,7 @@
   12.83          val _ = if_debug pth hth
   12.84          val th1 = implies_elim_all (beta_eta_thm th)
   12.85          val a = case concl_of th1 of
   12.86 -                    _ $ (Const("op -->",_) $ a $ Const("False",_)) => a
   12.87 +                    _ $ (Const(@{const_name "op -->"},_) $ a $ Const(@{const_name "False"},_)) => a
   12.88                    | _ => raise ERR "NOT_INTRO" "Conclusion of bad form"
   12.89          val ca = cterm_of thy a
   12.90          val th2 = Thm.equal_elim (Drule.instantiate' [] [SOME ca] not_intro_thm) th1
   12.91 @@ -1877,7 +1877,7 @@
   12.92          val _ = if_debug pth hth
   12.93          val th1 = implies_elim_all (beta_eta_thm th)
   12.94          val a = case concl_of th1 of
   12.95 -                    _ $ (Const("Not",_) $ a) => a
   12.96 +                    _ $ (Const(@{const_name "Not"},_) $ a) => a
   12.97                    | _ => raise ERR "NOT_ELIM" "Conclusion of bad form"
   12.98          val ca = cterm_of thy a
   12.99          val th2 = Thm.equal_elim (Drule.instantiate' [] [SOME ca] not_elim_thm) th1
  12.100 @@ -1996,7 +1996,7 @@
  12.101                                         ("x",dT,body $ Bound 0)
  12.102                                     end
  12.103                                     handle TYPE _ => raise ERR "new_specification" "not an abstraction type"
  12.104 -                               fun dest_exists (Const("Ex",_) $ abody) =
  12.105 +                               fun dest_exists (Const(@{const_name "Ex"},_) $ abody) =
  12.106                                     dest_eta_abs abody
  12.107                                   | dest_exists tm =
  12.108                                     raise ERR "new_specification" "Bad existential formula"
  12.109 @@ -2082,7 +2082,7 @@
  12.110              val (HOLThm(rens,td_th)) = norm_hthm thy hth
  12.111              val th2 = beta_eta_thm (td_th RS ex_imp_nonempty)
  12.112              val c = case concl_of th2 of
  12.113 -                        _ $ (Const("Ex",_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
  12.114 +                        _ $ (Const(@{const_name "Ex"},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
  12.115                        | _ => raise ERR "new_type_definition" "Bad type definition theorem"
  12.116              val tfrees = OldTerm.term_tfrees c
  12.117              val tnames = map fst tfrees
  12.118 @@ -2108,7 +2108,7 @@
  12.119              val rew = rewrite_hol4_term (concl_of td_th) thy4
  12.120              val th  = Thm.equal_elim rew (Thm.transfer thy4 td_th)
  12.121              val c   = case HOLogic.dest_Trueprop (prop_of th) of
  12.122 -                          Const("Ex",exT) $ P =>
  12.123 +                          Const(@{const_name "Ex"},exT) $ P =>
  12.124                            let
  12.125                                val PT = domain_type exT
  12.126                            in
  12.127 @@ -2157,7 +2157,7 @@
  12.128                                      SOME (cterm_of thy t)] light_nonempty
  12.129              val th2 = beta_eta_thm (td_th RS (beta_eta_thm light_nonempty'))
  12.130              val c = case concl_of th2 of
  12.131 -                        _ $ (Const("Ex",_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
  12.132 +                        _ $ (Const(@{const_name "Ex"},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
  12.133                        | _ => raise ERR "type_introduction" "Bad type definition theorem"
  12.134              val tfrees = OldTerm.term_tfrees c
  12.135              val tnames = sort_strings (map fst tfrees)
    13.1 --- a/src/HOL/Import/shuffler.ML	Thu Aug 19 10:27:12 2010 +0200
    13.2 +++ b/src/HOL/Import/shuffler.ML	Thu Aug 19 11:02:14 2010 +0200
    13.3 @@ -60,14 +60,14 @@
    13.4  
    13.5  fun mk_meta_eq th =
    13.6      (case concl_of th of
    13.7 -         Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th RS eq_reflection
    13.8 +         Const(@{const_name "Trueprop"},_) $ (Const(@{const_name "op ="},_) $ _ $ _) => th RS eq_reflection
    13.9         | Const("==",_) $ _ $ _ => th
   13.10         | _ => raise THM("Not an equality",0,[th]))
   13.11      handle _ => raise THM("Couldn't make meta equality",0,[th])  (* FIXME avoid handle _ *)
   13.12  
   13.13  fun mk_obj_eq th =
   13.14      (case concl_of th of
   13.15 -         Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th
   13.16 +         Const(@{const_name "Trueprop"},_) $ (Const(@{const_name "op ="},_) $ _ $ _) => th
   13.17         | Const("==",_) $ _ $ _ => th RS meta_eq_to_obj_eq
   13.18         | _ => raise THM("Not an equality",0,[th]))
   13.19      handle _ => raise THM("Couldn't make object equality",0,[th])  (* FIXME avoid handle _ *)
    14.1 --- a/src/HOL/Library/Eval_Witness.thy	Thu Aug 19 10:27:12 2010 +0200
    14.2 +++ b/src/HOL/Library/Eval_Witness.thy	Thu Aug 19 11:02:14 2010 +0200
    14.3 @@ -63,7 +63,7 @@
    14.4      else error ("Type " ^ quote (Syntax.string_of_typ_global thy T) ^ " not allowed for ML witnesses")
    14.5  
    14.6    fun dest_exs  0 t = t
    14.7 -    | dest_exs n (Const ("Ex", _) $ Abs (v,T,b)) = 
    14.8 +    | dest_exs n (Const (@{const_name "Ex"}, _) $ Abs (v,T,b)) = 
    14.9        Abs (v, check_type T, dest_exs (n - 1) b)
   14.10      | dest_exs _ _ = sys_error "dest_exs";
   14.11    val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
    15.1 --- a/src/HOL/Library/positivstellensatz.ML	Thu Aug 19 10:27:12 2010 +0200
    15.2 +++ b/src/HOL/Library/positivstellensatz.ML	Thu Aug 19 11:02:14 2010 +0200
    15.3 @@ -498,7 +498,7 @@
    15.4   val strip_exists =
    15.5    let fun h (acc, t) =
    15.6     case (term_of t) of
    15.7 -    Const("Ex",_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
    15.8 +    Const(@{const_name "Ex"},_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
    15.9    | _ => (acc,t)
   15.10    in fn t => h ([],t)
   15.11    end
   15.12 @@ -515,7 +515,7 @@
   15.13   fun mk_ex v t = Thm.capply (ext (ctyp_of_term v)) (Thm.cabs v t)
   15.14  
   15.15   fun choose v th th' = case concl_of th of 
   15.16 -   @{term Trueprop} $ (Const("Ex",_)$_) => 
   15.17 +   @{term Trueprop} $ (Const(@{const_name "Ex"},_)$_) => 
   15.18      let
   15.19       val p = (funpow 2 Thm.dest_arg o cprop_of) th
   15.20       val T = (hd o Thm.dest_ctyp o ctyp_of_term) p
   15.21 @@ -533,7 +533,7 @@
   15.22   val strip_forall =
   15.23    let fun h (acc, t) =
   15.24     case (term_of t) of
   15.25 -    Const("All",_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
   15.26 +    Const(@{const_name "All"},_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
   15.27    | _ => (acc,t)
   15.28    in fn t => h ([],t)
   15.29    end
    16.1 --- a/src/HOL/Library/reflection.ML	Thu Aug 19 10:27:12 2010 +0200
    16.2 +++ b/src/HOL/Library/reflection.ML	Thu Aug 19 11:02:14 2010 +0200
    16.3 @@ -82,7 +82,7 @@
    16.4  fun rearrange congs =
    16.5    let
    16.6      fun P (_, th) =
    16.7 -      let val @{term "Trueprop"}$(Const ("op =",_) $l$_) = concl_of th
    16.8 +      let val @{term "Trueprop"}$(Const (@{const_name "op ="},_) $l$_) = concl_of th
    16.9        in can dest_Var l end
   16.10      val (yes,no) = List.partition P congs
   16.11    in no @ yes end
    17.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Thu Aug 19 10:27:12 2010 +0200
    17.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Thu Aug 19 11:02:14 2010 +0200
    17.3 @@ -183,7 +183,7 @@
    17.4    end;
    17.5  
    17.6  fun mk_not_sym ths = maps (fn th => case prop_of th of
    17.7 -    _ $ (Const ("Not", _) $ (Const ("op =", _) $ _ $ _)) => [th, th RS not_sym]
    17.8 +    _ $ (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _)) => [th, th RS not_sym]
    17.9    | _ => [th]) ths;
   17.10  
   17.11  fun fresh_const T U = Const ("Nominal.fresh", T --> U --> HOLogic.boolT);
   17.12 @@ -1372,7 +1372,7 @@
   17.13                              SUBGOAL (fn (t, i) => case Logic.strip_assums_concl t of
   17.14                                  _ $ (Const ("Nominal.fresh", _) $ _ $ _) =>
   17.15                                    simp_tac ind_ss1' i
   17.16 -                              | _ $ (Const ("Not", _) $ _) =>
   17.17 +                              | _ $ (Const (@{const_name "Not"}, _) $ _) =>
   17.18                                    resolve_tac freshs2' i
   17.19                                | _ => asm_simp_tac (HOL_basic_ss addsimps
   17.20                                    pt2_atoms addsimprocs [perm_simproc]) i)) 1])
   17.21 @@ -1671,7 +1671,7 @@
   17.22      val rec_unique_frees' =
   17.23        Datatype_Prop.indexify_names (replicate (length recTs) "y") ~~ rec_result_Ts;
   17.24      val rec_unique_concls = map (fn ((x, U), R) =>
   17.25 -        Const ("Ex1", (U --> HOLogic.boolT) --> HOLogic.boolT) $
   17.26 +        Const (@{const_name "Ex1"}, (U --> HOLogic.boolT) --> HOLogic.boolT) $
   17.27            Abs ("y", U, R $ Free x $ Bound 0))
   17.28        (rec_unique_frees ~~ rec_result_Ts ~~ rec_sets);
   17.29  
   17.30 @@ -1777,7 +1777,7 @@
   17.31                        | _ => false) prems';
   17.32                      val fresh_prems = filter (fn th => case prop_of th of
   17.33                          _ $ (Const ("Nominal.fresh", _) $ _ $ _) => true
   17.34 -                      | _ $ (Const ("Not", _) $ _) => true
   17.35 +                      | _ $ (Const (@{const_name "Not"}, _) $ _) => true
   17.36                        | _ => false) prems';
   17.37                      val Ts = map fastype_of boundsl;
   17.38  
   17.39 @@ -1879,7 +1879,7 @@
   17.40                        end) rec_prems2;
   17.41  
   17.42                      val ihs = filter (fn th => case prop_of th of
   17.43 -                      _ $ (Const ("All", _) $ _) => true | _ => false) prems';
   17.44 +                      _ $ (Const (@{const_name "All"}, _) $ _) => true | _ => false) prems';
   17.45  
   17.46                      (** pi1 o rs = pi2 o vs , rs = pi1^-1 o pi2 o vs **)
   17.47                      val _ = warning "step 7: pi1 o rs = pi2 o vs , rs = pi1^-1 o pi2 o vs";
   17.48 @@ -2022,7 +2022,7 @@
   17.49            (reccomb_names ~~ recTs ~~ rec_result_Ts))
   17.50        |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
   17.51            (Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
   17.52 -           Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
   17.53 +           Const (@{const_name "The"}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
   17.54               set $ Free ("x", T) $ Free ("y", T'))))))
   17.55                 (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts));
   17.56  
    18.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Thu Aug 19 10:27:12 2010 +0200
    18.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Aug 19 11:02:14 2010 +0200
    18.3 @@ -71,14 +71,14 @@
    18.4    | add_binders thy i (Abs (_, _, t)) bs = add_binders thy (i + 1) t bs
    18.5    | add_binders thy i _ bs = bs;
    18.6  
    18.7 -fun split_conj f names (Const ("op &", _) $ p $ q) _ = (case head_of p of
    18.8 +fun split_conj f names (Const (@{const_name "op &"}, _) $ p $ q) _ = (case head_of p of
    18.9        Const (name, _) =>
   18.10          if member (op =) names name then SOME (f p q) else NONE
   18.11      | _ => NONE)
   18.12    | split_conj _ _ _ _ = NONE;
   18.13  
   18.14  fun strip_all [] t = t
   18.15 -  | strip_all (_ :: xs) (Const ("All", _) $ Abs (s, T, t)) = strip_all xs t;
   18.16 +  | strip_all (_ :: xs) (Const (@{const_name "All"}, _) $ Abs (s, T, t)) = strip_all xs t;
   18.17  
   18.18  (*********************************************************************)
   18.19  (* maps  R ... & (ALL pi_1 ... pi_n z. P z (pi_1 o ... o pi_n o t))  *)
   18.20 @@ -89,7 +89,7 @@
   18.21  (* where "id" protects the subformula from simplification            *)
   18.22  (*********************************************************************)
   18.23  
   18.24 -fun inst_conj_all names ps pis (Const ("op &", _) $ p $ q) _ =
   18.25 +fun inst_conj_all names ps pis (Const (@{const_name "op &"}, _) $ p $ q) _ =
   18.26        (case head_of p of
   18.27           Const (name, _) =>
   18.28             if member (op =) names name then SOME (HOLogic.mk_conj (p,
    19.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Thu Aug 19 10:27:12 2010 +0200
    19.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Thu Aug 19 11:02:14 2010 +0200
    19.3 @@ -75,14 +75,14 @@
    19.4    | add_binders thy i (Abs (_, _, t)) bs = add_binders thy (i + 1) t bs
    19.5    | add_binders thy i _ bs = bs;
    19.6  
    19.7 -fun split_conj f names (Const ("op &", _) $ p $ q) _ = (case head_of p of
    19.8 +fun split_conj f names (Const (@{const_name "op &"}, _) $ p $ q) _ = (case head_of p of
    19.9        Const (name, _) =>
   19.10          if member (op =) names name then SOME (f p q) else NONE
   19.11      | _ => NONE)
   19.12    | split_conj _ _ _ _ = NONE;
   19.13  
   19.14  fun strip_all [] t = t
   19.15 -  | strip_all (_ :: xs) (Const ("All", _) $ Abs (s, T, t)) = strip_all xs t;
   19.16 +  | strip_all (_ :: xs) (Const (@{const_name "All"}, _) $ Abs (s, T, t)) = strip_all xs t;
   19.17  
   19.18  (*********************************************************************)
   19.19  (* maps  R ... & (ALL pi_1 ... pi_n z. P z (pi_1 o ... o pi_n o t))  *)
   19.20 @@ -93,7 +93,7 @@
   19.21  (* where "id" protects the subformula from simplification            *)
   19.22  (*********************************************************************)
   19.23  
   19.24 -fun inst_conj_all names ps pis (Const ("op &", _) $ p $ q) _ =
   19.25 +fun inst_conj_all names ps pis (Const (@{const_name "op &"}, _) $ p $ q) _ =
   19.26        (case head_of p of
   19.27           Const (name, _) =>
   19.28             if member (op =) names name then SOME (HOLogic.mk_conj (p,
    20.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML	Thu Aug 19 10:27:12 2010 +0200
    20.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML	Thu Aug 19 11:02:14 2010 +0200
    20.3 @@ -135,7 +135,7 @@
    20.4      val thy = Context.theory_of context
    20.5      val thms_to_be_added = (case (prop_of orig_thm) of
    20.6          (* case: eqvt-lemma is of the implicational form *)
    20.7 -        (Const("==>", _) $ (Const ("Trueprop",_) $ hyp) $ (Const ("Trueprop",_) $ concl)) =>
    20.8 +        (Const("==>", _) $ (Const (@{const_name "Trueprop"},_) $ hyp) $ (Const (@{const_name "Trueprop"},_) $ concl)) =>
    20.9            let
   20.10              val (pi,typi) = get_pi concl thy
   20.11            in
    21.1 --- a/src/HOL/Prolog/prolog.ML	Thu Aug 19 10:27:12 2010 +0200
    21.2 +++ b/src/HOL/Prolog/prolog.ML	Thu Aug 19 11:02:14 2010 +0200
    21.3 @@ -10,17 +10,17 @@
    21.4  exception not_HOHH;
    21.5  
    21.6  fun isD t = case t of
    21.7 -    Const("Trueprop",_)$t     => isD t
    21.8 -  | Const("op &"  ,_)$l$r     => isD l andalso isD r
    21.9 -  | Const("op -->",_)$l$r     => isG l andalso isD r
   21.10 +    Const(@{const_name "Trueprop"},_)$t     => isD t
   21.11 +  | Const(@{const_name "op &"}  ,_)$l$r     => isD l andalso isD r
   21.12 +  | Const(@{const_name "op -->"},_)$l$r     => isG l andalso isD r
   21.13    | Const(   "==>",_)$l$r     => isG l andalso isD r
   21.14 -  | Const("All",_)$Abs(s,_,t) => isD t
   21.15 +  | Const(@{const_name "All"},_)$Abs(s,_,t) => isD t
   21.16    | Const("all",_)$Abs(s,_,t) => isD t
   21.17 -  | Const("op |",_)$_$_       => false
   21.18 -  | Const("Ex" ,_)$_          => false
   21.19 +  | Const(@{const_name "op |"},_)$_$_       => false
   21.20 +  | Const(@{const_name "Ex"} ,_)$_          => false
   21.21    | Const("not",_)$_          => false
   21.22 -  | Const("True",_)           => false
   21.23 -  | Const("False",_)          => false
   21.24 +  | Const(@{const_name "True"},_)           => false
   21.25 +  | Const(@{const_name "False"},_)          => false
   21.26    | l $ r                     => isD l
   21.27    | Const _ (* rigid atom *)  => true
   21.28    | Bound _ (* rigid atom *)  => true
   21.29 @@ -29,17 +29,17 @@
   21.30              anything else *)  => false
   21.31  and
   21.32      isG t = case t of
   21.33 -    Const("Trueprop",_)$t     => isG t
   21.34 -  | Const("op &"  ,_)$l$r     => isG l andalso isG r
   21.35 -  | Const("op |"  ,_)$l$r     => isG l andalso isG r
   21.36 -  | Const("op -->",_)$l$r     => isD l andalso isG r
   21.37 +    Const(@{const_name "Trueprop"},_)$t     => isG t
   21.38 +  | Const(@{const_name "op &"}  ,_)$l$r     => isG l andalso isG r
   21.39 +  | Const(@{const_name "op |"}  ,_)$l$r     => isG l andalso isG r
   21.40 +  | Const(@{const_name "op -->"},_)$l$r     => isD l andalso isG r
   21.41    | Const(   "==>",_)$l$r     => isD l andalso isG r
   21.42 -  | Const("All",_)$Abs(_,_,t) => isG t
   21.43 +  | Const(@{const_name "All"},_)$Abs(_,_,t) => isG t
   21.44    | Const("all",_)$Abs(_,_,t) => isG t
   21.45 -  | Const("Ex" ,_)$Abs(_,_,t) => isG t
   21.46 -  | Const("True",_)           => true
   21.47 +  | Const(@{const_name "Ex"} ,_)$Abs(_,_,t) => isG t
   21.48 +  | Const(@{const_name "True"},_)           => true
   21.49    | Const("not",_)$_          => false
   21.50 -  | Const("False",_)          => false
   21.51 +  | Const(@{const_name "False"},_)          => false
   21.52    | _ (* atom *)              => true;
   21.53  
   21.54  val check_HOHH_tac1 = PRIMITIVE (fn thm =>
   21.55 @@ -51,10 +51,10 @@
   21.56  
   21.57  fun atomizeD ctxt thm = let
   21.58      fun at  thm = case concl_of thm of
   21.59 -      _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS
   21.60 +      _$(Const(@{const_name "All"} ,_)$Abs(s,_,_))=> at(thm RS
   21.61          (read_instantiate ctxt [(("x", 0), "?" ^ (if s="P" then "PP" else s))] spec))
   21.62 -    | _$(Const("op &",_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
   21.63 -    | _$(Const("op -->",_)$_$_)     => at(thm RS mp)
   21.64 +    | _$(Const(@{const_name "op &"},_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
   21.65 +    | _$(Const(@{const_name "op -->"},_)$_$_)     => at(thm RS mp)
   21.66      | _                             => [thm]
   21.67  in map zero_var_indexes (at thm) end;
   21.68  
   21.69 @@ -71,15 +71,15 @@
   21.70                                    resolve_tac (maps atomizeD prems) 1);
   21.71    -- is nice, but cannot instantiate unknowns in the assumptions *)
   21.72  fun hyp_resolve_tac i st = let
   21.73 -        fun ap (Const("All",_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a  ,t))
   21.74 -        |   ap (Const("op -->",_)$_$t)    =(case ap t of (k,_,t) => (k,true ,t))
   21.75 +        fun ap (Const(@{const_name "All"},_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a  ,t))
   21.76 +        |   ap (Const(@{const_name "op -->"},_)$_$t)    =(case ap t of (k,_,t) => (k,true ,t))
   21.77          |   ap t                          =                         (0,false,t);
   21.78  (*
   21.79          fun rep_goal (Const ("all",_)$Abs (_,_,t)) = rep_goal t
   21.80          |   rep_goal (Const ("==>",_)$s$t)         =
   21.81                          (case rep_goal t of (l,t) => (s::l,t))
   21.82          |   rep_goal t                             = ([]  ,t);
   21.83 -        val (prems, Const("Trueprop", _)$concl) = rep_goal
   21.84 +        val (prems, Const(@{const_name "Trueprop"}, _)$concl) = rep_goal
   21.85                                                  (#3(dest_state (st,i)));
   21.86  *)
   21.87          val subgoal = #3(Thm.dest_state (st,i));
    22.1 --- a/src/HOL/Statespace/distinct_tree_prover.ML	Thu Aug 19 10:27:12 2010 +0200
    22.2 +++ b/src/HOL/Statespace/distinct_tree_prover.ML	Thu Aug 19 11:02:14 2010 +0200
    22.3 @@ -343,7 +343,7 @@
    22.4    end handle Option => NONE)
    22.5  
    22.6  fun distinctTree_tac names ctxt 
    22.7 -      (Const ("Trueprop",_) $ (Const ("Not", _) $ (Const ("op =", _) $ x $ y)), i) =
    22.8 +      (Const (@{const_name "Trueprop"},_) $ (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op ="}, _) $ x $ y)), i) =
    22.9    (case get_fst_success (neq_x_y ctxt x y) names of
   22.10       SOME neq => rtac neq i
   22.11     | NONE => no_tac)
   22.12 @@ -356,7 +356,7 @@
   22.13  
   22.14  fun distinct_simproc names =
   22.15    Simplifier.simproc @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"]
   22.16 -    (fn thy => fn ss => fn (Const ("op =",_)$x$y) =>
   22.17 +    (fn thy => fn ss => fn (Const (@{const_name "op ="},_)$x$y) =>
   22.18          case try Simplifier.the_context ss of
   22.19          SOME ctxt => Option.map (fn neq => neq_to_eq_False OF [neq]) 
   22.20                        (get_fst_success (neq_x_y ctxt x y) names)
    23.1 --- a/src/HOL/Statespace/state_fun.ML	Thu Aug 19 10:27:12 2010 +0200
    23.2 +++ b/src/HOL/Statespace/state_fun.ML	Thu Aug 19 11:02:14 2010 +0200
    23.3 @@ -43,9 +43,9 @@
    23.4  val conj_True = thm "conj_True";
    23.5  val conj_cong = thm "conj_cong";
    23.6  
    23.7 -fun isFalse (Const ("False",_)) = true
    23.8 +fun isFalse (Const (@{const_name "False"},_)) = true
    23.9    | isFalse _ = false;
   23.10 -fun isTrue (Const ("True",_)) = true
   23.11 +fun isTrue (Const (@{const_name "True"},_)) = true
   23.12    | isTrue _ = false;
   23.13  
   23.14  in
   23.15 @@ -53,7 +53,7 @@
   23.16  val lazy_conj_simproc =
   23.17    Simplifier.simproc @{theory HOL} "lazy_conj_simp" ["P & Q"]
   23.18      (fn thy => fn ss => fn t =>
   23.19 -      (case t of (Const ("op &",_)$P$Q) => 
   23.20 +      (case t of (Const (@{const_name "op &"},_)$P$Q) => 
   23.21           let
   23.22              val P_P' = Simplifier.rewrite ss (cterm_of thy P);
   23.23              val P' = P_P' |> prop_of |> Logic.dest_equals |> #2 
   23.24 @@ -285,7 +285,7 @@
   23.25                              then Bound 2
   23.26                              else raise TERM ("",[n]);
   23.27                     val sel' = lo $ d $ n' $ s;
   23.28 -                  in (Const ("op =",Teq)$sel'$x',hd (binder_types Teq),nT,swap) end;
   23.29 +                  in (Const (@{const_name "op ="},Teq)$sel'$x',hd (binder_types Teq),nT,swap) end;
   23.30  
   23.31           fun dest_state (s as Bound 0) = s
   23.32             | dest_state (s as (Const (sel,sT)$Bound 0)) =
   23.33 @@ -295,20 +295,20 @@
   23.34             | dest_state s = 
   23.35                      raise TERM ("StateFun.ex_lookup_eq_simproc: not a record slector",[s]);
   23.36    
   23.37 -         fun dest_sel_eq (Const ("op =",Teq)$
   23.38 +         fun dest_sel_eq (Const (@{const_name "op ="},Teq)$
   23.39                             ((lo as (Const ("StateFun.lookup",lT)))$d$n$s)$X) =
   23.40                             (false,Teq,lT,lo,d,n,X,dest_state s)
   23.41 -           | dest_sel_eq (Const ("op =",Teq)$X$
   23.42 +           | dest_sel_eq (Const (@{const_name "op ="},Teq)$X$
   23.43                              ((lo as (Const ("StateFun.lookup",lT)))$d$n$s)) =
   23.44                             (true,Teq,lT,lo,d,n,X,dest_state s)
   23.45             | dest_sel_eq _ = raise TERM ("",[]);
   23.46  
   23.47         in
   23.48           (case t of
   23.49 -           (Const ("Ex",Tex)$Abs(s,T,t)) =>
   23.50 +           (Const (@{const_name "Ex"},Tex)$Abs(s,T,t)) =>
   23.51               (let val (eq,eT,nT,swap) = mkeq (dest_sel_eq t) 0;
   23.52                    val prop = list_all ([("n",nT),("x",eT)],
   23.53 -                              Logic.mk_equals (Const ("Ex",Tex)$Abs(s,T,eq),
   23.54 +                              Logic.mk_equals (Const (@{const_name "Ex"},Tex)$Abs(s,T,eq),
   23.55                                                 HOLogic.true_const));
   23.56                    val thm = Drule.export_without_context (prove prop);
   23.57                    val thm' = if swap then swap_ex_eq OF [thm] else thm
   23.58 @@ -367,7 +367,7 @@
   23.59       val (lookup_ss,ex_lookup_ss,simprocs_active) = StateFunData.get ctxt;
   23.60       val (lookup_ss', ex_lookup_ss') = 
   23.61             (case (concl_of thm) of
   23.62 -            (_$((Const ("Ex",_)$_))) => (lookup_ss, ex_lookup_ss addsimps [thm])
   23.63 +            (_$((Const (@{const_name "Ex"},_)$_))) => (lookup_ss, ex_lookup_ss addsimps [thm])
   23.64              | _ => (lookup_ss addsimps [thm], ex_lookup_ss))
   23.65       fun activate_simprocs ctxt =
   23.66            if simprocs_active then ctxt
    24.1 --- a/src/HOL/Statespace/state_space.ML	Thu Aug 19 10:27:12 2010 +0200
    24.2 +++ b/src/HOL/Statespace/state_space.ML	Thu Aug 19 11:02:14 2010 +0200
    24.3 @@ -222,8 +222,8 @@
    24.4    end handle Option => NONE)
    24.5  
    24.6  fun distinctTree_tac ctxt
    24.7 -      (Const ("Trueprop",_) $
    24.8 -        (Const ("Not", _) $ (Const ("op =", _) $ (x as Free _)$ (y as Free _))), i) =
    24.9 +      (Const (@{const_name "Trueprop"},_) $
   24.10 +        (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op ="}, _) $ (x as Free _)$ (y as Free _))), i) =
   24.11    (case (neq_x_y ctxt x y) of
   24.12       SOME neq => rtac neq i
   24.13     | NONE => no_tac)
   24.14 @@ -236,7 +236,7 @@
   24.15  
   24.16  val distinct_simproc =
   24.17    Simplifier.simproc @{theory HOL} "StateSpace.distinct_simproc" ["x = y"]
   24.18 -    (fn thy => fn ss => (fn (Const ("op =",_)$(x as Free _)$(y as Free _)) =>
   24.19 +    (fn thy => fn ss => (fn (Const (@{const_name "op ="},_)$(x as Free _)$(y as Free _)) =>
   24.20          (case try Simplifier.the_context ss of
   24.21            SOME ctxt => Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq])
   24.22                         (neq_x_y ctxt x y)
    25.1 --- a/src/HOL/TLA/Intensional.thy	Thu Aug 19 10:27:12 2010 +0200
    25.2 +++ b/src/HOL/TLA/Intensional.thy	Thu Aug 19 11:02:14 2010 +0200
    25.3 @@ -279,7 +279,7 @@
    25.4  
    25.5      fun hflatten t =
    25.6          case (concl_of t) of
    25.7 -          Const _ $ (Const ("op -->", _) $ _ $ _) => hflatten (t RS mp)
    25.8 +          Const _ $ (Const (@{const_name "op -->"}, _) $ _ $ _) => hflatten (t RS mp)
    25.9          | _ => (hflatten (matchsome conjI t)) handle THM _ => zero_var_indexes t
   25.10    in
   25.11      hflatten t
    26.1 --- a/src/HOL/Tools/Function/function_core.ML	Thu Aug 19 10:27:12 2010 +0200
    26.2 +++ b/src/HOL/Tools/Function/function_core.ML	Thu Aug 19 11:02:14 2010 +0200
    26.3 @@ -392,7 +392,7 @@
    26.4      (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
    26.5      val ihyp = Term.all domT $ Abs ("z", domT,
    26.6        Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
    26.7 -        HOLogic.mk_Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
    26.8 +        HOLogic.mk_Trueprop (Const (@{const_name "Ex1"}, (ranT --> boolT) --> boolT) $
    26.9            Abs ("y", ranT, G $ Bound 1 $ Bound 0))))
   26.10        |> cterm_of thy
   26.11  
    27.1 --- a/src/HOL/Tools/Function/termination.ML	Thu Aug 19 10:27:12 2010 +0200
    27.2 +++ b/src/HOL/Tools/Function/termination.ML	Thu Aug 19 11:02:14 2010 +0200
    27.3 @@ -148,7 +148,7 @@
    27.4      val cs = Function_Lib.dest_binop_list @{const_name Lattices.sup} rel
    27.5      fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
    27.6        let
    27.7 -        val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
    27.8 +        val (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
    27.9            = Term.strip_qnt_body "Ex" c
   27.10        in cons r o cons l end
   27.11    in
   27.12 @@ -185,7 +185,7 @@
   27.13      val vs = Term.strip_qnt_vars "Ex" c
   27.14  
   27.15      (* FIXME: throw error "dest_call" for malformed terms *)
   27.16 -    val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
   27.17 +    val (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
   27.18        = Term.strip_qnt_body "Ex" c
   27.19      val (p, l') = dest_inj sk l
   27.20      val (q, r') = dest_inj sk r
    28.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Aug 19 10:27:12 2010 +0200
    28.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Aug 19 11:02:14 2010 +0200
    28.3 @@ -147,7 +147,7 @@
    28.4  
    28.5  fun Trueprop_conv cv ct =
    28.6    case Thm.term_of ct of
    28.7 -    Const ("Trueprop", _) $ _ => Conv.arg_conv cv ct  
    28.8 +    Const (@{const_name "Trueprop"}, _) $ _ => Conv.arg_conv cv ct  
    28.9    | _ => raise Fail "Trueprop_conv"
   28.10  
   28.11  fun preprocess_intro thy rule =
    29.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Aug 19 10:27:12 2010 +0200
    29.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Aug 19 11:02:14 2010 +0200
    29.3 @@ -405,13 +405,13 @@
    29.4  (* general syntactic functions *)
    29.5  
    29.6  (*Like dest_conj, but flattens conjunctions however nested*)
    29.7 -fun conjuncts_aux (Const ("op &", _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
    29.8 +fun conjuncts_aux (Const (@{const_name "op &"}, _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
    29.9    | conjuncts_aux t conjs = t::conjs;
   29.10  
   29.11  fun conjuncts t = conjuncts_aux t [];
   29.12  
   29.13  fun is_equationlike_term (Const ("==", _) $ _ $ _) = true
   29.14 -  | is_equationlike_term (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _)) = true
   29.15 +  | is_equationlike_term (Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _)) = true
   29.16    | is_equationlike_term _ = false
   29.17    
   29.18  val is_equationlike = is_equationlike_term o prop_of 
   29.19 @@ -482,7 +482,7 @@
   29.20  
   29.21  fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t)
   29.22  
   29.23 -fun strip_ex (Const ("Ex", _) $ Abs (x, T, t)) =
   29.24 +fun strip_ex (Const (@{const_name "Ex"}, _) $ Abs (x, T, t)) =
   29.25    let
   29.26      val (xTs, t') = strip_ex t
   29.27    in
    30.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Aug 19 10:27:12 2010 +0200
    30.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Aug 19 11:02:14 2010 +0200
    30.3 @@ -524,7 +524,7 @@
    30.4  
    30.5  fun dest_conjunct_prem th =
    30.6    case HOLogic.dest_Trueprop (prop_of th) of
    30.7 -    (Const ("op &", _) $ t $ t') =>
    30.8 +    (Const (@{const_name "op &"}, _) $ t $ t') =>
    30.9        dest_conjunct_prem (th RS @{thm conjunct1})
   30.10          @ dest_conjunct_prem (th RS @{thm conjunct2})
   30.11      | _ => [th]
   30.12 @@ -576,7 +576,7 @@
   30.13  
   30.14  fun Trueprop_conv cv ct =
   30.15    case Thm.term_of ct of
   30.16 -    Const ("Trueprop", _) $ _ => Conv.arg_conv cv ct  
   30.17 +    Const (@{const_name "Trueprop"}, _) $ _ => Conv.arg_conv cv ct  
   30.18    | _ => raise Fail "Trueprop_conv"
   30.19  
   30.20  fun preprocess_intro thy rule =
   30.21 @@ -587,7 +587,7 @@
   30.22  
   30.23  fun preprocess_elim ctxt elimrule =
   30.24    let
   30.25 -    fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) =
   30.26 +    fun replace_eqs (Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, T) $ lhs $ rhs)) =
   30.27         HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
   30.28       | replace_eqs t = t
   30.29      val thy = ProofContext.theory_of ctxt
    31.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu Aug 19 10:27:12 2010 +0200
    31.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu Aug 19 11:02:14 2010 +0200
    31.3 @@ -111,7 +111,7 @@
    31.4  
    31.5  fun mk_meta_equation th =
    31.6    case prop_of th of
    31.7 -    Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _) => th RS @{thm eq_reflection}
    31.8 +    Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _) => th RS @{thm eq_reflection}
    31.9    | _ => th
   31.10  
   31.11  val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp}
    32.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Thu Aug 19 10:27:12 2010 +0200
    32.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Thu Aug 19 11:02:14 2010 +0200
    32.3 @@ -86,11 +86,11 @@
    32.4     map instantiate rew_ths
    32.5   end
    32.6  
    32.7 -fun is_compound ((Const ("Not", _)) $ t) =
    32.8 +fun is_compound ((Const (@{const_name "Not"}, _)) $ t) =
    32.9      error "is_compound: Negation should not occur; preprocessing is defect"
   32.10 -  | is_compound ((Const ("Ex", _)) $ _) = true
   32.11 +  | is_compound ((Const (@{const_name "Ex"}, _)) $ _) = true
   32.12    | is_compound ((Const (@{const_name "op |"}, _)) $ _ $ _) = true
   32.13 -  | is_compound ((Const ("op &", _)) $ _ $ _) =
   32.14 +  | is_compound ((Const (@{const_name "op &"}, _)) $ _ $ _) =
   32.15      error "is_compound: Conjunction should not occur; preprocessing is defect"
   32.16    | is_compound _ = false
   32.17  
    33.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Aug 19 10:27:12 2010 +0200
    33.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Aug 19 11:02:14 2010 +0200
    33.3 @@ -168,10 +168,10 @@
    33.4      mk_split_lambda' xs t
    33.5    end;
    33.6  
    33.7 -fun strip_imp_prems (Const("op -->", _) $ A $ B) = A :: strip_imp_prems B
    33.8 +fun strip_imp_prems (Const(@{const_name "op -->"}, _) $ A $ B) = A :: strip_imp_prems B
    33.9    | strip_imp_prems _ = [];
   33.10  
   33.11 -fun strip_imp_concl (Const("op -->", _) $ A $ B) = strip_imp_concl B
   33.12 +fun strip_imp_concl (Const(@{const_name "op -->"}, _) $ A $ B) = strip_imp_concl B
   33.13    | strip_imp_concl A = A : term;
   33.14  
   33.15  fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
    34.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Thu Aug 19 10:27:12 2010 +0200
    34.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Thu Aug 19 11:02:14 2010 +0200
    34.3 @@ -120,10 +120,10 @@
    34.4  
    34.5  fun whatis x ct =
    34.6  ( case (term_of ct) of
    34.7 -  Const("op &",_)$_$_ => And (Thm.dest_binop ct)
    34.8 -| Const ("op |",_)$_$_ => Or (Thm.dest_binop ct)
    34.9 -| Const ("op =",_)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
   34.10 -| Const (@{const_name Not},_) $ (Const ("op =",_)$y$_) =>
   34.11 +  Const(@{const_name "op &"},_)$_$_ => And (Thm.dest_binop ct)
   34.12 +| Const (@{const_name "op |"},_)$_$_ => Or (Thm.dest_binop ct)
   34.13 +| Const (@{const_name "op ="},_)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
   34.14 +| Const (@{const_name Not},_) $ (Const (@{const_name "op ="},_)$y$_) =>
   34.15    if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox
   34.16  | Const (@{const_name Orderings.less}, _) $ y$ z =>
   34.17     if term_of x aconv y then Lt (Thm.dest_arg ct)
   34.18 @@ -274,7 +274,7 @@
   34.19    | lin vs (Const (@{const_name Not},T)$t) = Const (@{const_name Not},T)$ (lin vs t)
   34.20    | lin (vs as x::_) (Const(@{const_name Rings.dvd},_)$d$t) =
   34.21      HOLogic.mk_binrel @{const_name Rings.dvd} (numeral1 abs d, lint vs t)
   34.22 -  | lin (vs as x::_) ((b as Const("op =",_))$s$t) =
   34.23 +  | lin (vs as x::_) ((b as Const(@{const_name "op ="},_))$s$t) =
   34.24       (case lint vs (subC$t$s) of
   34.25        (t as a$(m$c$y)$r) =>
   34.26          if x <> y then b$zero$t
   34.27 @@ -353,8 +353,8 @@
   34.28      then (ins (dest_number c) acc, dacc) else (acc,dacc)
   34.29    | Const(@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$y)$_) =>
   34.30      if x aconv y then (acc,ins (dest_number c) dacc) else (acc,dacc)
   34.31 -  | Const("op &",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
   34.32 -  | Const("op |",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
   34.33 +  | Const(@{const_name "op &"},_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
   34.34 +  | Const(@{const_name "op |"},_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
   34.35    | Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t)
   34.36    | _ => (acc, dacc)
   34.37    val (cs,ds) = h ([],[]) p
   34.38 @@ -382,8 +382,8 @@
   34.39      end
   34.40    fun unit_conv t =
   34.41     case (term_of t) of
   34.42 -   Const("op &",_)$_$_ => Conv.binop_conv unit_conv t
   34.43 -  | Const("op |",_)$_$_ => Conv.binop_conv unit_conv t
   34.44 +   Const(@{const_name "op &"},_)$_$_ => Conv.binop_conv unit_conv t
   34.45 +  | Const(@{const_name "op |"},_)$_$_ => Conv.binop_conv unit_conv t
   34.46    | Const (@{const_name Not},_)$_ => Conv.arg_conv unit_conv t
   34.47    | Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
   34.48      if x=y andalso member (op =)
   34.49 @@ -612,19 +612,19 @@
   34.50  
   34.51  fun fm_of_term ps vs (Const (@{const_name True}, _)) = Proc.T
   34.52    | fm_of_term ps vs (Const (@{const_name False}, _)) = Proc.F
   34.53 -  | fm_of_term ps vs (Const ("op &", _) $ t1 $ t2) =
   34.54 +  | fm_of_term ps vs (Const (@{const_name "op &"}, _) $ t1 $ t2) =
   34.55        Proc.And (fm_of_term ps vs t1, fm_of_term ps vs t2)
   34.56 -  | fm_of_term ps vs (Const ("op |", _) $ t1 $ t2) =
   34.57 +  | fm_of_term ps vs (Const (@{const_name "op |"}, _) $ t1 $ t2) =
   34.58        Proc.Or (fm_of_term ps vs t1, fm_of_term ps vs t2)
   34.59 -  | fm_of_term ps vs (Const ("op -->", _) $ t1 $ t2) =
   34.60 +  | fm_of_term ps vs (Const (@{const_name "op -->"}, _) $ t1 $ t2) =
   34.61        Proc.Imp (fm_of_term ps vs t1, fm_of_term ps vs t2)
   34.62    | fm_of_term ps vs (@{term "op = :: bool => _ "} $ t1 $ t2) =
   34.63        Proc.Iff (fm_of_term ps vs t1, fm_of_term ps vs t2)
   34.64    | fm_of_term ps vs (Const (@{const_name Not}, _) $ t') =
   34.65        Proc.Not (fm_of_term ps vs t')
   34.66 -  | fm_of_term ps vs (Const ("Ex", _) $ Abs abs) =
   34.67 +  | fm_of_term ps vs (Const (@{const_name "Ex"}, _) $ Abs abs) =
   34.68        Proc.E (uncurry (fm_of_term ps) (descend vs abs))
   34.69 -  | fm_of_term ps vs (Const ("All", _) $ Abs abs) =
   34.70 +  | fm_of_term ps vs (Const (@{const_name "All"}, _) $ Abs abs) =
   34.71        Proc.A (uncurry (fm_of_term ps) (descend vs abs))
   34.72    | fm_of_term ps vs (@{term "op = :: int => _"} $ t1 $ t2) =
   34.73        Proc.Eq (Proc.Sub (num_of_term vs t1, num_of_term vs t2))
   34.74 @@ -687,14 +687,14 @@
   34.75  
   34.76  fun strip_objimp ct =
   34.77    (case Thm.term_of ct of
   34.78 -    Const ("op -->", _) $ _ $ _ =>
   34.79 +    Const (@{const_name "op -->"}, _) $ _ $ _ =>
   34.80        let val (A, B) = Thm.dest_binop ct
   34.81        in A :: strip_objimp B end
   34.82    | _ => [ct]);
   34.83  
   34.84  fun strip_objall ct = 
   34.85   case term_of ct of 
   34.86 -  Const ("All", _) $ Abs (xn,xT,p) => 
   34.87 +  Const (@{const_name "All"}, _) $ Abs (xn,xT,p) => 
   34.88     let val (a,(v,t')) = (apsnd (Thm.dest_abs (SOME xn)) o Thm.dest_comb) ct
   34.89     in apfst (cons (a,v)) (strip_objall t')
   34.90     end
    35.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Aug 19 10:27:12 2010 +0200
    35.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Aug 19 11:02:14 2010 +0200
    35.3 @@ -308,7 +308,7 @@
    35.4                    SOME w =>  mk_var(w, dummyT)
    35.5                  | NONE   => mk_var(v, dummyT))
    35.6          | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
    35.7 -            Const ("op =", HOLogic.typeT)
    35.8 +            Const (@{const_name "op ="}, HOLogic.typeT)
    35.9          | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
   35.10             (case strip_prefix_and_undo_ascii const_prefix x of
   35.11                  SOME c => Const (invert_const c, dummyT)
    36.1 --- a/src/HOL/Tools/TFL/post.ML	Thu Aug 19 10:27:12 2010 +0200
    36.2 +++ b/src/HOL/Tools/TFL/post.ML	Thu Aug 19 11:02:14 2010 +0200
    36.3 @@ -67,7 +67,7 @@
    36.4  val P_imp_P_eq_True = @{thm eqTrueI} RS eq_reflection;
    36.5  fun mk_meta_eq r = case concl_of r of
    36.6       Const("==",_)$_$_ => r
    36.7 -  |   _ $(Const("op =",_)$_$_) => r RS eq_reflection
    36.8 +  |   _ $(Const(@{const_name "op ="},_)$_$_) => r RS eq_reflection
    36.9    |   _ => r RS P_imp_P_eq_True
   36.10  
   36.11  (*Is this the best way to invoke the simplifier??*)
    37.1 --- a/src/HOL/Tools/TFL/rules.ML	Thu Aug 19 10:27:12 2010 +0200
    37.2 +++ b/src/HOL/Tools/TFL/rules.ML	Thu Aug 19 11:02:14 2010 +0200
    37.3 @@ -453,14 +453,14 @@
    37.4  (* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *)
    37.5  fun is_cong thm =
    37.6    case (Thm.prop_of thm)
    37.7 -     of (Const("==>",_)$(Const("Trueprop",_)$ _) $
    37.8 +     of (Const("==>",_)$(Const(@{const_name "Trueprop"},_)$ _) $
    37.9           (Const("==",_) $ (Const (@{const_name Recdef.cut},_) $ f $ R $ a $ x) $ _)) => false
   37.10        | _ => true;
   37.11  
   37.12  
   37.13  fun dest_equal(Const ("==",_) $
   37.14 -               (Const ("Trueprop",_) $ lhs)
   37.15 -               $ (Const ("Trueprop",_) $ rhs)) = {lhs=lhs, rhs=rhs}
   37.16 +               (Const (@{const_name "Trueprop"},_) $ lhs)
   37.17 +               $ (Const (@{const_name "Trueprop"},_) $ rhs)) = {lhs=lhs, rhs=rhs}
   37.18    | dest_equal(Const ("==",_) $ lhs $ rhs)  = {lhs=lhs, rhs=rhs}
   37.19    | dest_equal tm = S.dest_eq tm;
   37.20  
   37.21 @@ -759,7 +759,7 @@
   37.22                val cntxt = rev(Simplifier.prems_of_ss ss)
   37.23                val dummy = print_thms "cntxt:" cntxt
   37.24                val thy = Thm.theory_of_thm thm
   37.25 -              val Const("==>",_) $ (Const("Trueprop",_) $ A) $ _ = Thm.prop_of thm
   37.26 +              val Const("==>",_) $ (Const(@{const_name "Trueprop"},_) $ A) $ _ = Thm.prop_of thm
   37.27                fun genl tm = let val vlist = subtract (op aconv) globals
   37.28                                             (OldTerm.add_term_frees(tm,[]))
   37.29                              in fold_rev Forall vlist tm
    38.1 --- a/src/HOL/Tools/TFL/tfl.ML	Thu Aug 19 10:27:12 2010 +0200
    38.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Thu Aug 19 11:02:14 2010 +0200
    38.3 @@ -483,7 +483,7 @@
    38.4       val (case_rewrites,context_congs) = extraction_thms thy
    38.5       val tych = Thry.typecheck thy
    38.6       val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
    38.7 -     val Const("All",_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
    38.8 +     val Const(@{const_name "All"},_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
    38.9       val R = Free (Name.variant (List.foldr OldTerm.add_term_names [] eqns) Rname,
   38.10                     Rtype)
   38.11       val WFREC_THM = R.ISPECL [tych R, tych g] WFREC_THM0
    39.1 --- a/src/HOL/Tools/TFL/usyntax.ML	Thu Aug 19 10:27:12 2010 +0200
    39.2 +++ b/src/HOL/Tools/TFL/usyntax.ML	Thu Aug 19 11:02:14 2010 +0200
    39.3 @@ -159,7 +159,7 @@
    39.4  
    39.5  
    39.6  fun mk_imp{ant,conseq} =
    39.7 -   let val c = Const("op -->",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
    39.8 +   let val c = Const(@{const_name "op -->"},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
    39.9     in list_comb(c,[ant,conseq])
   39.10     end;
   39.11  
   39.12 @@ -171,24 +171,24 @@
   39.13  
   39.14  fun mk_forall (r as {Bvar,Body}) =
   39.15    let val ty = type_of Bvar
   39.16 -      val c = Const("All",(ty --> HOLogic.boolT) --> HOLogic.boolT)
   39.17 +      val c = Const(@{const_name "All"},(ty --> HOLogic.boolT) --> HOLogic.boolT)
   39.18    in list_comb(c,[mk_abs r])
   39.19    end;
   39.20  
   39.21  fun mk_exists (r as {Bvar,Body}) =
   39.22    let val ty = type_of Bvar
   39.23 -      val c = Const("Ex",(ty --> HOLogic.boolT) --> HOLogic.boolT)
   39.24 +      val c = Const(@{const_name "Ex"},(ty --> HOLogic.boolT) --> HOLogic.boolT)
   39.25    in list_comb(c,[mk_abs r])
   39.26    end;
   39.27  
   39.28  
   39.29  fun mk_conj{conj1,conj2} =
   39.30 -   let val c = Const("op &",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
   39.31 +   let val c = Const(@{const_name "op &"},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
   39.32     in list_comb(c,[conj1,conj2])
   39.33     end;
   39.34  
   39.35  fun mk_disj{disj1,disj2} =
   39.36 -   let val c = Const("op |",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
   39.37 +   let val c = Const(@{const_name "op |"},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
   39.38     in list_comb(c,[disj1,disj2])
   39.39     end;
   39.40  
   39.41 @@ -244,25 +244,25 @@
   39.42       end
   39.43    | dest_abs _ _ =  raise USYN_ERR "dest_abs" "not an abstraction";
   39.44  
   39.45 -fun dest_eq(Const("op =",_) $ M $ N) = {lhs=M, rhs=N}
   39.46 +fun dest_eq(Const(@{const_name "op ="},_) $ M $ N) = {lhs=M, rhs=N}
   39.47    | dest_eq _ = raise USYN_ERR "dest_eq" "not an equality";
   39.48  
   39.49 -fun dest_imp(Const("op -->",_) $ M $ N) = {ant=M, conseq=N}
   39.50 +fun dest_imp(Const(@{const_name "op -->"},_) $ M $ N) = {ant=M, conseq=N}
   39.51    | dest_imp _ = raise USYN_ERR "dest_imp" "not an implication";
   39.52  
   39.53 -fun dest_forall(Const("All",_) $ (a as Abs _)) = fst (dest_abs [] a)
   39.54 +fun dest_forall(Const(@{const_name "All"},_) $ (a as Abs _)) = fst (dest_abs [] a)
   39.55    | dest_forall _ = raise USYN_ERR "dest_forall" "not a forall";
   39.56  
   39.57 -fun dest_exists(Const("Ex",_) $ (a as Abs _)) = fst (dest_abs [] a)
   39.58 +fun dest_exists(Const(@{const_name "Ex"},_) $ (a as Abs _)) = fst (dest_abs [] a)
   39.59    | dest_exists _ = raise USYN_ERR "dest_exists" "not an existential";
   39.60  
   39.61  fun dest_neg(Const("not",_) $ M) = M
   39.62    | dest_neg _ = raise USYN_ERR "dest_neg" "not a negation";
   39.63  
   39.64 -fun dest_conj(Const("op &",_) $ M $ N) = {conj1=M, conj2=N}
   39.65 +fun dest_conj(Const(@{const_name "op &"},_) $ M $ N) = {conj1=M, conj2=N}
   39.66    | dest_conj _ = raise USYN_ERR "dest_conj" "not a conjunction";
   39.67  
   39.68 -fun dest_disj(Const("op |",_) $ M $ N) = {disj1=M, disj2=N}
   39.69 +fun dest_disj(Const(@{const_name "op |"},_) $ M $ N) = {disj1=M, disj2=N}
   39.70    | dest_disj _ = raise USYN_ERR "dest_disj" "not a disjunction";
   39.71  
   39.72  fun mk_pair{fst,snd} =
   39.73 @@ -402,6 +402,6 @@
   39.74    | is_WFR _                 = false;
   39.75  
   39.76  fun ARB ty = mk_select{Bvar=Free("v",ty),
   39.77 -                       Body=Const("True",HOLogic.boolT)};
   39.78 +                       Body=Const(@{const_name "True"},HOLogic.boolT)};
   39.79  
   39.80  end;
    40.1 --- a/src/HOL/Tools/choice_specification.ML	Thu Aug 19 10:27:12 2010 +0200
    40.2 +++ b/src/HOL/Tools/choice_specification.ML	Thu Aug 19 11:02:14 2010 +0200
    40.3 @@ -24,7 +24,7 @@
    40.4      fun mk_definitional [] arg = arg
    40.5        | mk_definitional ((thname,cname,covld)::cos) (thy,thm) =
    40.6          case HOLogic.dest_Trueprop (concl_of thm) of
    40.7 -            Const("Ex",_) $ P =>
    40.8 +            Const(@{const_name "Ex"},_) $ P =>
    40.9              let
   40.10                  val ctype = domain_type (type_of P)
   40.11                  val cname_full = Sign.intern_const thy cname
   40.12 @@ -51,7 +51,7 @@
   40.13                  end
   40.14                | process ((thname,cname,covld)::cos) (thy,tm) =
   40.15                  case tm of
   40.16 -                    Const("Ex",_) $ P =>
   40.17 +                    Const(@{const_name "Ex"},_) $ P =>
   40.18                      let
   40.19                          val ctype = domain_type (type_of P)
   40.20                          val cname_full = Sign.intern_const thy cname
    41.1 --- a/src/HOL/Tools/cnf_funcs.ML	Thu Aug 19 10:27:12 2010 +0200
    41.2 +++ b/src/HOL/Tools/cnf_funcs.ML	Thu Aug 19 11:02:14 2010 +0200
    41.3 @@ -93,19 +93,19 @@
    41.4  
    41.5  val cnftac_eq_imp        = @{lemma "[| P = Q; P |] ==> Q" by auto};
    41.6  
    41.7 -fun is_atom (Const ("False", _))                                           = false
    41.8 -  | is_atom (Const ("True", _))                                            = false
    41.9 -  | is_atom (Const ("op &", _) $ _ $ _)                                    = false
   41.10 -  | is_atom (Const ("op |", _) $ _ $ _)                                    = false
   41.11 -  | is_atom (Const ("op -->", _) $ _ $ _)                                  = false
   41.12 -  | is_atom (Const ("op =", Type ("fun", Type ("bool", []) :: _)) $ _ $ _) = false
   41.13 -  | is_atom (Const ("Not", _) $ _)                                         = false
   41.14 +fun is_atom (Const (@{const_name "False"}, _))                                           = false
   41.15 +  | is_atom (Const (@{const_name "True"}, _))                                            = false
   41.16 +  | is_atom (Const (@{const_name "op &"}, _) $ _ $ _)                                    = false
   41.17 +  | is_atom (Const (@{const_name "op |"}, _) $ _ $ _)                                    = false
   41.18 +  | is_atom (Const (@{const_name "op -->"}, _) $ _ $ _)                                  = false
   41.19 +  | is_atom (Const (@{const_name "op ="}, Type ("fun", Type ("bool", []) :: _)) $ _ $ _) = false
   41.20 +  | is_atom (Const (@{const_name "Not"}, _) $ _)                                         = false
   41.21    | is_atom _                                                              = true;
   41.22  
   41.23 -fun is_literal (Const ("Not", _) $ x) = is_atom x
   41.24 +fun is_literal (Const (@{const_name "Not"}, _) $ x) = is_atom x
   41.25    | is_literal x                      = is_atom x;
   41.26  
   41.27 -fun is_clause (Const ("op |", _) $ x $ y) = is_clause x andalso is_clause y
   41.28 +fun is_clause (Const (@{const_name "op |"}, _) $ x $ y) = is_clause x andalso is_clause y
   41.29    | is_clause x                           = is_literal x;
   41.30  
   41.31  (* ------------------------------------------------------------------------- *)
   41.32 @@ -118,7 +118,7 @@
   41.33  fun clause_is_trivial c =
   41.34  	let
   41.35  		(* Term.term -> Term.term *)
   41.36 -		fun dual (Const ("Not", _) $ x) = x
   41.37 +		fun dual (Const (@{const_name "Not"}, _) $ x) = x
   41.38  		  | dual x                      = HOLogic.Not $ x
   41.39  		(* Term.term list -> bool *)
   41.40  		fun has_duals []      = false
   41.41 @@ -184,28 +184,28 @@
   41.42  
   41.43  (* Theory.theory -> Term.term -> Thm.thm *)
   41.44  
   41.45 -fun make_nnf_thm thy (Const ("op &", _) $ x $ y) =
   41.46 +fun make_nnf_thm thy (Const (@{const_name "op &"}, _) $ x $ y) =
   41.47  	let
   41.48  		val thm1 = make_nnf_thm thy x
   41.49  		val thm2 = make_nnf_thm thy y
   41.50  	in
   41.51  		conj_cong OF [thm1, thm2]
   41.52  	end
   41.53 -  | make_nnf_thm thy (Const ("op |", _) $ x $ y) =
   41.54 +  | make_nnf_thm thy (Const (@{const_name "op |"}, _) $ x $ y) =
   41.55  	let
   41.56  		val thm1 = make_nnf_thm thy x
   41.57  		val thm2 = make_nnf_thm thy y
   41.58  	in
   41.59  		disj_cong OF [thm1, thm2]
   41.60  	end
   41.61 -  | make_nnf_thm thy (Const ("op -->", _) $ x $ y) =
   41.62 +  | make_nnf_thm thy (Const (@{const_name "op -->"}, _) $ x $ y) =
   41.63  	let
   41.64  		val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
   41.65  		val thm2 = make_nnf_thm thy y
   41.66  	in
   41.67  		make_nnf_imp OF [thm1, thm2]
   41.68  	end
   41.69 -  | make_nnf_thm thy (Const ("op =", Type ("fun", Type ("bool", []) :: _)) $ x $ y) =
   41.70 +  | make_nnf_thm thy (Const (@{const_name "op ="}, Type ("fun", Type ("bool", []) :: _)) $ x $ y) =
   41.71  	let
   41.72  		val thm1 = make_nnf_thm thy x
   41.73  		val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
   41.74 @@ -214,32 +214,32 @@
   41.75  	in
   41.76  		make_nnf_iff OF [thm1, thm2, thm3, thm4]
   41.77  	end
   41.78 -  | make_nnf_thm thy (Const ("Not", _) $ Const ("False", _)) =
   41.79 +  | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ Const (@{const_name "False"}, _)) =
   41.80  	make_nnf_not_false
   41.81 -  | make_nnf_thm thy (Const ("Not", _) $ Const ("True", _)) =
   41.82 +  | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ Const (@{const_name "True"}, _)) =
   41.83  	make_nnf_not_true
   41.84 -  | make_nnf_thm thy (Const ("Not", _) $ (Const ("op &", _) $ x $ y)) =
   41.85 +  | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op &"}, _) $ x $ y)) =
   41.86  	let
   41.87  		val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
   41.88  		val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
   41.89  	in
   41.90  		make_nnf_not_conj OF [thm1, thm2]
   41.91  	end
   41.92 -  | make_nnf_thm thy (Const ("Not", _) $ (Const ("op |", _) $ x $ y)) =
   41.93 +  | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op |"}, _) $ x $ y)) =
   41.94  	let
   41.95  		val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
   41.96  		val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
   41.97  	in
   41.98  		make_nnf_not_disj OF [thm1, thm2]
   41.99  	end
  41.100 -  | make_nnf_thm thy (Const ("Not", _) $ (Const ("op -->", _) $ x $ y)) =
  41.101 +  | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op -->"}, _) $ x $ y)) =
  41.102  	let
  41.103  		val thm1 = make_nnf_thm thy x
  41.104  		val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
  41.105  	in
  41.106  		make_nnf_not_imp OF [thm1, thm2]
  41.107  	end
  41.108 -  | make_nnf_thm thy (Const ("Not", _) $ (Const ("op =", Type ("fun", Type ("bool", []) :: _)) $ x $ y)) =
  41.109 +  | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op ="}, Type ("fun", Type ("bool", []) :: _)) $ x $ y)) =
  41.110  	let
  41.111  		val thm1 = make_nnf_thm thy x
  41.112  		val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
  41.113 @@ -248,7 +248,7 @@
  41.114  	in
  41.115  		make_nnf_not_iff OF [thm1, thm2, thm3, thm4]
  41.116  	end
  41.117 -  | make_nnf_thm thy (Const ("Not", _) $ (Const ("Not", _) $ x)) =
  41.118 +  | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "Not"}, _) $ x)) =
  41.119  	let
  41.120  		val thm1 = make_nnf_thm thy x
  41.121  	in
  41.122 @@ -276,7 +276,7 @@
  41.123  
  41.124  (* Theory.theory -> Term.term -> Thm.thm *)
  41.125  
  41.126 -fun simp_True_False_thm thy (Const ("op &", _) $ x $ y) =
  41.127 +fun simp_True_False_thm thy (Const (@{const_name "op &"}, _) $ x $ y) =
  41.128  	let
  41.129  		val thm1 = simp_True_False_thm thy x
  41.130  		val x'   = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
  41.131 @@ -298,7 +298,7 @@
  41.132  					conj_cong OF [thm1, thm2]  (* (x & y) = (x' & y') *)
  41.133  			end
  41.134  	end
  41.135 -  | simp_True_False_thm thy (Const ("op |", _) $ x $ y) =
  41.136 +  | simp_True_False_thm thy (Const (@{const_name "op |"}, _) $ x $ y) =
  41.137  	let
  41.138  		val thm1 = simp_True_False_thm thy x
  41.139  		val x'   = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
  41.140 @@ -334,24 +334,24 @@
  41.141  fun make_cnf_thm thy t =
  41.142  let
  41.143  	(* Term.term -> Thm.thm *)
  41.144 -	fun make_cnf_thm_from_nnf (Const ("op &", _) $ x $ y) =
  41.145 +	fun make_cnf_thm_from_nnf (Const (@{const_name "op &"}, _) $ x $ y) =
  41.146  		let
  41.147  			val thm1 = make_cnf_thm_from_nnf x
  41.148  			val thm2 = make_cnf_thm_from_nnf y
  41.149  		in
  41.150  			conj_cong OF [thm1, thm2]
  41.151  		end
  41.152 -	  | make_cnf_thm_from_nnf (Const ("op |", _) $ x $ y) =
  41.153 +	  | make_cnf_thm_from_nnf (Const (@{const_name "op |"}, _) $ x $ y) =
  41.154  		let
  41.155  			(* produces a theorem "(x' | y') = t'", where x', y', and t' are in CNF *)
  41.156 -			fun make_cnf_disj_thm (Const ("op &", _) $ x1 $ x2) y' =
  41.157 +			fun make_cnf_disj_thm (Const (@{const_name "op &"}, _) $ x1 $ x2) y' =
  41.158  				let
  41.159  					val thm1 = make_cnf_disj_thm x1 y'
  41.160  					val thm2 = make_cnf_disj_thm x2 y'
  41.161  				in
  41.162  					make_cnf_disj_conj_l OF [thm1, thm2]  (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
  41.163  				end
  41.164 -			  | make_cnf_disj_thm x' (Const ("op &", _) $ y1 $ y2) =
  41.165 +			  | make_cnf_disj_thm x' (Const (@{const_name "op &"}, _) $ y1 $ y2) =
  41.166  				let
  41.167  					val thm1 = make_cnf_disj_thm x' y1
  41.168  					val thm2 = make_cnf_disj_thm x' y2
  41.169 @@ -403,34 +403,34 @@
  41.170  	val var_id = Unsynchronized.ref 0  (* properly initialized below *)
  41.171  	fun new_free () =
  41.172  		Free ("cnfx_" ^ string_of_int (Unsynchronized.inc var_id), HOLogic.boolT)
  41.173 -	fun make_cnfx_thm_from_nnf (Const ("op &", _) $ x $ y) : thm =
  41.174 +	fun make_cnfx_thm_from_nnf (Const (@{const_name "op &"}, _) $ x $ y) : thm =
  41.175  		let
  41.176  			val thm1 = make_cnfx_thm_from_nnf x
  41.177  			val thm2 = make_cnfx_thm_from_nnf y
  41.178  		in
  41.179  			conj_cong OF [thm1, thm2]
  41.180  		end
  41.181 -	  | make_cnfx_thm_from_nnf (Const ("op |", _) $ x $ y) =
  41.182 +	  | make_cnfx_thm_from_nnf (Const (@{const_name "op |"}, _) $ x $ y) =
  41.183  		if is_clause x andalso is_clause y then
  41.184  			inst_thm thy [HOLogic.mk_disj (x, y)] iff_refl
  41.185  		else if is_literal y orelse is_literal x then let
  41.186  			(* produces a theorem "(x' | y') = t'", where x', y', and t' are *)
  41.187  			(* almost in CNF, and x' or y' is a literal                      *)
  41.188 -			fun make_cnfx_disj_thm (Const ("op &", _) $ x1 $ x2) y' =
  41.189 +			fun make_cnfx_disj_thm (Const (@{const_name "op &"}, _) $ x1 $ x2) y' =
  41.190  				let
  41.191  					val thm1 = make_cnfx_disj_thm x1 y'
  41.192  					val thm2 = make_cnfx_disj_thm x2 y'
  41.193  				in
  41.194  					make_cnf_disj_conj_l OF [thm1, thm2]  (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
  41.195  				end
  41.196 -			  | make_cnfx_disj_thm x' (Const ("op &", _) $ y1 $ y2) =
  41.197 +			  | make_cnfx_disj_thm x' (Const (@{const_name "op &"}, _) $ y1 $ y2) =
  41.198  				let
  41.199  					val thm1 = make_cnfx_disj_thm x' y1
  41.200  					val thm2 = make_cnfx_disj_thm x' y2
  41.201  				in
  41.202  					make_cnf_disj_conj_r OF [thm1, thm2]  (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
  41.203  				end
  41.204 -			  | make_cnfx_disj_thm (Const ("Ex", _) $ x') y' =
  41.205 +			  | make_cnfx_disj_thm (Const (@{const_name "Ex"}, _) $ x') y' =
  41.206  				let
  41.207  					val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_l   (* ((Ex x') | y') = (Ex (x' | y')) *)
  41.208  					val var  = new_free ()
  41.209 @@ -441,7 +441,7 @@
  41.210  				in
  41.211  					iff_trans OF [thm1, thm5]  (* ((Ex x') | y') = (Ex v. body') *)
  41.212  				end
  41.213 -			  | make_cnfx_disj_thm x' (Const ("Ex", _) $ y') =
  41.214 +			  | make_cnfx_disj_thm x' (Const (@{const_name "Ex"}, _) $ y') =
  41.215  				let
  41.216  					val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_r   (* (x' | (Ex y')) = (Ex (x' | y')) *)
  41.217  					val var  = new_free ()
    42.1 --- a/src/HOL/Tools/groebner.ML	Thu Aug 19 10:27:12 2010 +0200
    42.2 +++ b/src/HOL/Tools/groebner.ML	Thu Aug 19 11:02:14 2010 +0200
    42.3 @@ -395,7 +395,7 @@
    42.4  
    42.5  fun refute_disj rfn tm =
    42.6   case term_of tm of
    42.7 -  Const("op |",_)$l$r =>
    42.8 +  Const(@{const_name "op |"},_)$l$r =>
    42.9     compose_single(refute_disj rfn (dest_arg tm),2,compose_single(refute_disj rfn (dest_arg1 tm),2,disjE))
   42.10    | _ => rfn tm ;
   42.11  
   42.12 @@ -405,11 +405,11 @@
   42.13  val mk_comb = capply;
   42.14  fun is_neg t =
   42.15      case term_of t of
   42.16 -      (Const("Not",_)$p) => true
   42.17 +      (Const(@{const_name "Not"},_)$p) => true
   42.18      | _  => false;
   42.19  fun is_eq t =
   42.20   case term_of t of
   42.21 - (Const("op =",_)$_$_) => true
   42.22 + (Const(@{const_name "op ="},_)$_$_) => true
   42.23  | _  => false;
   42.24  
   42.25  fun end_itlist f l =
   42.26 @@ -430,14 +430,14 @@
   42.27  val strip_exists =
   42.28   let fun h (acc, t) =
   42.29        case (term_of t) of
   42.30 -       Const("Ex",_)$Abs(x,T,p) => h (dest_abs NONE (dest_arg t) |>> (fn v => v::acc))
   42.31 +       Const(@{const_name "Ex"},_)$Abs(x,T,p) => h (dest_abs NONE (dest_arg t) |>> (fn v => v::acc))
   42.32       | _ => (acc,t)
   42.33   in fn t => h ([],t)
   42.34   end;
   42.35  
   42.36  fun is_forall t =
   42.37   case term_of t of
   42.38 -  (Const("All",_)$Abs(_,_,_)) => true
   42.39 +  (Const(@{const_name "All"},_)$Abs(_,_,_)) => true
   42.40  | _ => false;
   42.41  
   42.42  val mk_object_eq = fn th => th COMP meta_eq_to_obj_eq;
   42.43 @@ -522,7 +522,7 @@
   42.44   fun mk_ex v t = Thm.capply (ext (ctyp_of_term v)) (Thm.cabs v t)
   42.45  
   42.46  fun choose v th th' = case concl_of th of 
   42.47 -  @{term Trueprop} $ (Const("Ex",_)$_) => 
   42.48 +  @{term Trueprop} $ (Const(@{const_name "Ex"},_)$_) => 
   42.49     let
   42.50      val p = (funpow 2 Thm.dest_arg o cprop_of) th
   42.51      val T = (hd o Thm.dest_ctyp o ctyp_of_term) p
   42.52 @@ -923,15 +923,15 @@
   42.53  
   42.54  fun find_term bounds tm =
   42.55    (case term_of tm of
   42.56 -    Const ("op =", T) $ _ $ _ =>
   42.57 +    Const (@{const_name "op ="}, T) $ _ $ _ =>
   42.58        if domain_type T = HOLogic.boolT then find_args bounds tm
   42.59        else dest_arg tm
   42.60 -  | Const ("Not", _) $ _ => find_term bounds (dest_arg tm)
   42.61 -  | Const ("All", _) $ _ => find_body bounds (dest_arg tm)
   42.62 -  | Const ("Ex", _) $ _ => find_body bounds (dest_arg tm)
   42.63 -  | Const ("op &", _) $ _ $ _ => find_args bounds tm
   42.64 -  | Const ("op |", _) $ _ $ _ => find_args bounds tm
   42.65 -  | Const ("op -->", _) $ _ $ _ => find_args bounds tm
   42.66 +  | Const (@{const_name "Not"}, _) $ _ => find_term bounds (dest_arg tm)
   42.67 +  | Const (@{const_name "All"}, _) $ _ => find_body bounds (dest_arg tm)
   42.68 +  | Const (@{const_name "Ex"}, _) $ _ => find_body bounds (dest_arg tm)
   42.69 +  | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
   42.70 +  | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
   42.71 +  | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
   42.72    | @{term "op ==>"} $_$_ => find_args bounds tm
   42.73    | Const("op ==",_)$_$_ => find_args bounds tm
   42.74    | @{term Trueprop}$_ => find_term bounds (dest_arg tm)
   42.75 @@ -985,7 +985,7 @@
   42.76  
   42.77  local
   42.78   fun lhs t = case term_of t of
   42.79 -  Const("op =",_)$_$_ => Thm.dest_arg1 t
   42.80 +  Const(@{const_name "op ="},_)$_$_ => Thm.dest_arg1 t
   42.81   | _=> raise CTERM ("ideal_tac - lhs",[t])
   42.82   fun exitac NONE = no_tac
   42.83     | exitac (SOME y) = rtac (instantiate' [SOME (ctyp_of_term y)] [NONE,SOME y] exI) 1
    43.1 --- a/src/HOL/Tools/lin_arith.ML	Thu Aug 19 10:27:12 2010 +0200
    43.2 +++ b/src/HOL/Tools/lin_arith.ML	Thu Aug 19 11:02:14 2010 +0200
    43.3 @@ -46,12 +46,12 @@
    43.4  val mk_Trueprop = HOLogic.mk_Trueprop;
    43.5  
    43.6  fun atomize thm = case Thm.prop_of thm of
    43.7 -    Const ("Trueprop", _) $ (Const (@{const_name "op &"}, _) $ _ $ _) =>
    43.8 +    Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op &"}, _) $ _ $ _) =>
    43.9      atomize (thm RS conjunct1) @ atomize (thm RS conjunct2)
   43.10    | _ => [thm];
   43.11  
   43.12 -fun neg_prop ((TP as Const("Trueprop", _)) $ (Const (@{const_name Not}, _) $ t)) = TP $ t
   43.13 -  | neg_prop ((TP as Const("Trueprop", _)) $ t) = TP $ (HOLogic.Not $t)
   43.14 +fun neg_prop ((TP as Const(@{const_name "Trueprop"}, _)) $ (Const (@{const_name Not}, _) $ t)) = TP $ t
   43.15 +  | neg_prop ((TP as Const(@{const_name "Trueprop"}, _)) $ t) = TP $ (HOLogic.Not $t)
   43.16    | neg_prop t = raise TERM ("neg_prop", [t]);
   43.17  
   43.18  fun is_False thm =
   43.19 @@ -258,10 +258,10 @@
   43.20    | negate NONE                        = NONE;
   43.21  
   43.22  fun decomp_negation data
   43.23 -  ((Const ("Trueprop", _)) $ (Const (rel, T) $ lhs $ rhs)) : decomp option =
   43.24 +  ((Const (@{const_name "Trueprop"}, _)) $ (Const (rel, T) $ lhs $ rhs)) : decomp option =
   43.25        decomp_typecheck data (T, (rel, lhs, rhs))
   43.26 -  | decomp_negation data ((Const ("Trueprop", _)) $
   43.27 -  (Const ("Not", _) $ (Const (rel, T) $ lhs $ rhs))) =
   43.28 +  | decomp_negation data ((Const (@{const_name "Trueprop"}, _)) $
   43.29 +  (Const (@{const_name "Not"}, _) $ (Const (rel, T) $ lhs $ rhs))) =
   43.30        negate (decomp_typecheck data (T, (rel, lhs, rhs)))
   43.31    | decomp_negation data _ =
   43.32        NONE;
   43.33 @@ -273,7 +273,7 @@
   43.34    in decomp_negation (thy, discrete, inj_consts) end;
   43.35  
   43.36  fun domain_is_nat (_ $ (Const (_, T) $ _ $ _))                      = nT T
   43.37 -  | domain_is_nat (_ $ (Const ("Not", _) $ (Const (_, T) $ _ $ _))) = nT T
   43.38 +  | domain_is_nat (_ $ (Const (@{const_name "Not"}, _) $ (Const (_, T) $ _ $ _))) = nT T
   43.39    | domain_is_nat _                                                 = false;
   43.40  
   43.41  
   43.42 @@ -428,7 +428,7 @@
   43.43          val t2'             = incr_boundvars 1 t2
   43.44          val t1_lt_t2        = Const (@{const_name Orderings.less},
   43.45                                  split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
   43.46 -        val t1_eq_t2_plus_d = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
   43.47 +        val t1_eq_t2_plus_d = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
   43.48                                  (Const (@{const_name Groups.plus},
   43.49                                    split_type --> split_type --> split_type) $ t2' $ d)
   43.50          val not_false       = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   43.51 @@ -448,7 +448,7 @@
   43.52                              (map (incr_boundvars 1) rev_terms)
   43.53          val terms2      = map (subst_term [(split_term, zero_nat)]) rev_terms
   43.54          val t1'         = incr_boundvars 1 t1
   43.55 -        val t1_eq_nat_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
   43.56 +        val t1_eq_nat_n = Const (@{const_name "op ="}, HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
   43.57                              (Const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) $ n)
   43.58          val t1_lt_zero  = Const (@{const_name Orderings.less},
   43.59                              HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
   43.60 @@ -472,13 +472,13 @@
   43.61                                          (map (incr_boundvars 2) rev_terms)
   43.62          val t1'                     = incr_boundvars 2 t1
   43.63          val t2'                     = incr_boundvars 2 t2
   43.64 -        val t2_eq_zero              = Const ("op =",
   43.65 +        val t2_eq_zero              = Const (@{const_name "op ="},
   43.66                                          split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
   43.67 -        val t2_neq_zero             = HOLogic.mk_not (Const ("op =",
   43.68 +        val t2_neq_zero             = HOLogic.mk_not (Const (@{const_name "op ="},
   43.69                                          split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
   43.70          val j_lt_t2                 = Const (@{const_name Orderings.less},
   43.71                                          split_type --> split_type--> HOLogic.boolT) $ j $ t2'
   43.72 -        val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
   43.73 +        val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
   43.74                                         (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
   43.75                                           (Const (@{const_name Groups.times},
   43.76                                             split_type --> split_type --> split_type) $ t2' $ i) $ j)
   43.77 @@ -504,13 +504,13 @@
   43.78                                          (map (incr_boundvars 2) rev_terms)
   43.79          val t1'                     = incr_boundvars 2 t1
   43.80          val t2'                     = incr_boundvars 2 t2
   43.81 -        val t2_eq_zero              = Const ("op =",
   43.82 +        val t2_eq_zero              = Const (@{const_name "op ="},
   43.83                                          split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
   43.84 -        val t2_neq_zero             = HOLogic.mk_not (Const ("op =",
   43.85 +        val t2_neq_zero             = HOLogic.mk_not (Const (@{const_name "op ="},
   43.86                                          split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
   43.87          val j_lt_t2                 = Const (@{const_name Orderings.less},
   43.88                                          split_type --> split_type--> HOLogic.boolT) $ j $ t2'
   43.89 -        val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
   43.90 +        val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
   43.91                                         (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
   43.92                                           (Const (@{const_name Groups.times},
   43.93                                             split_type --> split_type --> split_type) $ t2' $ i) $ j)
   43.94 @@ -542,7 +542,7 @@
   43.95                                          (map (incr_boundvars 2) rev_terms)
   43.96          val t1'                     = incr_boundvars 2 t1
   43.97          val t2'                     = incr_boundvars 2 t2
   43.98 -        val t2_eq_zero              = Const ("op =",
   43.99 +        val t2_eq_zero              = Const (@{const_name "op ="},
  43.100                                          split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
  43.101          val zero_lt_t2              = Const (@{const_name Orderings.less},
  43.102                                          split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
  43.103 @@ -556,7 +556,7 @@
  43.104                                          split_type --> split_type--> HOLogic.boolT) $ j $ t2'
  43.105          val t2_lt_j                 = Const (@{const_name Orderings.less},
  43.106                                          split_type --> split_type--> HOLogic.boolT) $ t2' $ j
  43.107 -        val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
  43.108 +        val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
  43.109                                         (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
  43.110                                           (Const (@{const_name Groups.times},
  43.111                                             split_type --> split_type --> split_type) $ t2' $ i) $ j)
  43.112 @@ -596,7 +596,7 @@
  43.113                                          (map (incr_boundvars 2) rev_terms)
  43.114          val t1'                     = incr_boundvars 2 t1
  43.115          val t2'                     = incr_boundvars 2 t2
  43.116 -        val t2_eq_zero              = Const ("op =",
  43.117 +        val t2_eq_zero              = Const (@{const_name "op ="},
  43.118                                          split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
  43.119          val zero_lt_t2              = Const (@{const_name Orderings.less},
  43.120                                          split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
  43.121 @@ -610,7 +610,7 @@
  43.122                                          split_type --> split_type--> HOLogic.boolT) $ j $ t2'
  43.123          val t2_lt_j                 = Const (@{const_name Orderings.less},
  43.124                                          split_type --> split_type--> HOLogic.boolT) $ t2' $ j
  43.125 -        val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
  43.126 +        val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
  43.127                                         (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
  43.128                                           (Const (@{const_name Groups.times},
  43.129                                             split_type --> split_type --> split_type) $ t2' $ i) $ j)
  43.130 @@ -659,7 +659,7 @@
  43.131  
  43.132  fun negated_term_occurs_positively (terms : term list) : bool =
  43.133    List.exists
  43.134 -    (fn (Trueprop $ (Const ("Not", _) $ t)) =>
  43.135 +    (fn (Trueprop $ (Const (@{const_name "Not"}, _) $ t)) =>
  43.136        member Pattern.aeconv terms (Trueprop $ t)
  43.137        | _ => false)
  43.138      terms;
    44.1 --- a/src/HOL/Tools/meson.ML	Thu Aug 19 10:27:12 2010 +0200
    44.2 +++ b/src/HOL/Tools/meson.ML	Thu Aug 19 11:02:14 2010 +0200
    44.3 @@ -149,21 +149,21 @@
    44.4  (*Are any of the logical connectives in "bs" present in the term?*)
    44.5  fun has_conns bs =
    44.6    let fun has (Const(a,_)) = false
    44.7 -        | has (Const("Trueprop",_) $ p) = has p
    44.8 -        | has (Const("Not",_) $ p) = has p
    44.9 -        | has (Const("op |",_) $ p $ q) = member (op =) bs "op |" orelse has p orelse has q
   44.10 -        | has (Const("op &",_) $ p $ q) = member (op =) bs "op &" orelse has p orelse has q
   44.11 -        | has (Const("All",_) $ Abs(_,_,p)) = member (op =) bs "All" orelse has p
   44.12 -        | has (Const("Ex",_) $ Abs(_,_,p)) = member (op =) bs "Ex" orelse has p
   44.13 +        | has (Const(@{const_name "Trueprop"},_) $ p) = has p
   44.14 +        | has (Const(@{const_name "Not"},_) $ p) = has p
   44.15 +        | has (Const(@{const_name "op |"},_) $ p $ q) = member (op =) bs "op |" orelse has p orelse has q
   44.16 +        | has (Const(@{const_name "op &"},_) $ p $ q) = member (op =) bs "op &" orelse has p orelse has q
   44.17 +        | has (Const(@{const_name "All"},_) $ Abs(_,_,p)) = member (op =) bs "All" orelse has p
   44.18 +        | has (Const(@{const_name "Ex"},_) $ Abs(_,_,p)) = member (op =) bs "Ex" orelse has p
   44.19          | has _ = false
   44.20    in  has  end;
   44.21  
   44.22  
   44.23  (**** Clause handling ****)
   44.24  
   44.25 -fun literals (Const("Trueprop",_) $ P) = literals P
   44.26 -  | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q
   44.27 -  | literals (Const("Not",_) $ P) = [(false,P)]
   44.28 +fun literals (Const(@{const_name "Trueprop"},_) $ P) = literals P
   44.29 +  | literals (Const(@{const_name "op |"},_) $ P $ Q) = literals P @ literals Q
   44.30 +  | literals (Const(@{const_name "Not"},_) $ P) = [(false,P)]
   44.31    | literals P = [(true,P)];
   44.32  
   44.33  (*number of literals in a term*)
   44.34 @@ -172,16 +172,16 @@
   44.35  
   44.36  (*** Tautology Checking ***)
   44.37  
   44.38 -fun signed_lits_aux (Const ("op |", _) $ P $ Q) (poslits, neglits) =
   44.39 +fun signed_lits_aux (Const (@{const_name "op |"}, _) $ P $ Q) (poslits, neglits) =
   44.40        signed_lits_aux Q (signed_lits_aux P (poslits, neglits))
   44.41 -  | signed_lits_aux (Const("Not",_) $ P) (poslits, neglits) = (poslits, P::neglits)
   44.42 +  | signed_lits_aux (Const(@{const_name "Not"},_) $ P) (poslits, neglits) = (poslits, P::neglits)
   44.43    | signed_lits_aux P (poslits, neglits) = (P::poslits, neglits);
   44.44  
   44.45  fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]);
   44.46  
   44.47  (*Literals like X=X are tautologous*)
   44.48 -fun taut_poslit (Const("op =",_) $ t $ u) = t aconv u
   44.49 -  | taut_poslit (Const("True",_)) = true
   44.50 +fun taut_poslit (Const(@{const_name "op ="},_) $ t $ u) = t aconv u
   44.51 +  | taut_poslit (Const(@{const_name "True"},_)) = true
   44.52    | taut_poslit _ = false;
   44.53  
   44.54  fun is_taut th =
   44.55 @@ -208,18 +208,18 @@
   44.56  fun refl_clause_aux 0 th = th
   44.57    | refl_clause_aux n th =
   44.58         case HOLogic.dest_Trueprop (concl_of th) of
   44.59 -          (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _) =>
   44.60 +          (Const (@{const_name "op |"}, _) $ (Const (@{const_name "op |"}, _) $ _ $ _) $ _) =>
   44.61              refl_clause_aux n (th RS disj_assoc)    (*isolate an atom as first disjunct*)
   44.62 -        | (Const ("op |", _) $ (Const("Not",_) $ (Const("op =",_) $ t $ u)) $ _) =>
   44.63 +        | (Const (@{const_name "op |"}, _) $ (Const(@{const_name "Not"},_) $ (Const(@{const_name "op ="},_) $ t $ u)) $ _) =>
   44.64              if eliminable(t,u)
   44.65              then refl_clause_aux (n-1) (th RS not_refl_disj_D)  (*Var inequation: delete*)
   44.66              else refl_clause_aux (n-1) (th RS disj_comm)  (*not between Vars: ignore*)
   44.67 -        | (Const ("op |", _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
   44.68 +        | (Const (@{const_name "op |"}, _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
   44.69          | _ => (*not a disjunction*) th;
   44.70  
   44.71 -fun notequal_lits_count (Const ("op |", _) $ P $ Q) =
   44.72 +fun notequal_lits_count (Const (@{const_name "op |"}, _) $ P $ Q) =
   44.73        notequal_lits_count P + notequal_lits_count Q
   44.74 -  | notequal_lits_count (Const("Not",_) $ (Const("op =",_) $ _ $ _)) = 1
   44.75 +  | notequal_lits_count (Const(@{const_name "Not"},_) $ (Const(@{const_name "op ="},_) $ _ $ _)) = 1
   44.76    | notequal_lits_count _ = 0;
   44.77  
   44.78  (*Simplify a clause by applying reflexivity to its negated equality literals*)
   44.79 @@ -266,26 +266,26 @@
   44.80    fun prod x y = if x < max_cl andalso y < max_cl then x*y else max_cl;
   44.81    
   44.82    (*Estimate the number of clauses in order to detect infeasible theorems*)
   44.83 -  fun signed_nclauses b (Const("Trueprop",_) $ t) = signed_nclauses b t
   44.84 -    | signed_nclauses b (Const("Not",_) $ t) = signed_nclauses (not b) t
   44.85 -    | signed_nclauses b (Const("op &",_) $ t $ u) =
   44.86 +  fun signed_nclauses b (Const(@{const_name "Trueprop"},_) $ t) = signed_nclauses b t
   44.87 +    | signed_nclauses b (Const(@{const_name "Not"},_) $ t) = signed_nclauses (not b) t
   44.88 +    | signed_nclauses b (Const(@{const_name "op &"},_) $ t $ u) =
   44.89          if b then sum (signed_nclauses b t) (signed_nclauses b u)
   44.90               else prod (signed_nclauses b t) (signed_nclauses b u)
   44.91 -    | signed_nclauses b (Const("op |",_) $ t $ u) =
   44.92 +    | signed_nclauses b (Const(@{const_name "op |"},_) $ t $ u) =
   44.93          if b then prod (signed_nclauses b t) (signed_nclauses b u)
   44.94               else sum (signed_nclauses b t) (signed_nclauses b u)
   44.95 -    | signed_nclauses b (Const("op -->",_) $ t $ u) =
   44.96 +    | signed_nclauses b (Const(@{const_name "op -->"},_) $ t $ u) =
   44.97          if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
   44.98               else sum (signed_nclauses (not b) t) (signed_nclauses b u)
   44.99 -    | signed_nclauses b (Const("op =", Type ("fun", [T, _])) $ t $ u) =
  44.100 +    | signed_nclauses b (Const(@{const_name "op ="}, Type ("fun", [T, _])) $ t $ u) =
  44.101          if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*)
  44.102              if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
  44.103                            (prod (signed_nclauses (not b) u) (signed_nclauses b t))
  44.104                   else sum (prod (signed_nclauses b t) (signed_nclauses b u))
  44.105                            (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u))
  44.106          else 1
  44.107 -    | signed_nclauses b (Const("Ex", _) $ Abs (_,_,t)) = signed_nclauses b t
  44.108 -    | signed_nclauses b (Const("All",_) $ Abs (_,_,t)) = signed_nclauses b t
  44.109 +    | signed_nclauses b (Const(@{const_name "Ex"}, _) $ Abs (_,_,t)) = signed_nclauses b t
  44.110 +    | signed_nclauses b (Const(@{const_name "All"},_) $ Abs (_,_,t)) = signed_nclauses b t
  44.111      | signed_nclauses _ _ = 1; (* literal *)
  44.112   in 
  44.113    signed_nclauses true t >= max_cl
  44.114 @@ -296,7 +296,7 @@
  44.115  local  
  44.116    val spec_var = Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec))));
  44.117    val spec_varT = #T (Thm.rep_cterm spec_var);
  44.118 -  fun name_of (Const ("All", _) $ Abs(x,_,_)) = x | name_of _ = Name.uu;
  44.119 +  fun name_of (Const (@{const_name "All"}, _) $ Abs(x,_,_)) = x | name_of _ = Name.uu;
  44.120  in  
  44.121    fun freeze_spec th ctxt =
  44.122      let
  44.123 @@ -334,15 +334,15 @@
  44.124          else if not (has_conns ["All","Ex","op &"] (prop_of th))
  44.125          then nodups ctxt th :: ths (*no work to do, terminate*)
  44.126          else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
  44.127 -            Const ("op &", _) => (*conjunction*)
  44.128 +            Const (@{const_name "op &"}, _) => (*conjunction*)
  44.129                  cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
  44.130 -          | Const ("All", _) => (*universal quantifier*)
  44.131 +          | Const (@{const_name "All"}, _) => (*universal quantifier*)
  44.132                  let val (th',ctxt') = freeze_spec th (!ctxtr)
  44.133                  in  ctxtr := ctxt'; cnf_aux (th', ths) end
  44.134 -          | Const ("Ex", _) =>
  44.135 +          | Const (@{const_name "Ex"}, _) =>
  44.136                (*existential quantifier: Insert Skolem functions*)
  44.137                cnf_aux (apply_skolem_theorem (th, skolem_ths), ths)
  44.138 -          | Const ("op |", _) =>
  44.139 +          | Const (@{const_name "op |"}, _) =>
  44.140                (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
  44.141                  all combinations of converting P, Q to CNF.*)
  44.142                let val tac =
  44.143 @@ -365,8 +365,8 @@
  44.144  
  44.145  (**** Generation of contrapositives ****)
  44.146  
  44.147 -fun is_left (Const ("Trueprop", _) $
  44.148 -               (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _)) = true
  44.149 +fun is_left (Const (@{const_name "Trueprop"}, _) $
  44.150 +               (Const (@{const_name "op |"}, _) $ (Const (@{const_name "op |"}, _) $ _ $ _) $ _)) = true
  44.151    | is_left _ = false;
  44.152  
  44.153  (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
  44.154 @@ -429,8 +429,8 @@
  44.155  
  44.156  fun rigid t = not (is_Var (head_of t));
  44.157  
  44.158 -fun ok4horn (Const ("Trueprop",_) $ (Const ("op |", _) $ t $ _)) = rigid t
  44.159 -  | ok4horn (Const ("Trueprop",_) $ t) = rigid t
  44.160 +fun ok4horn (Const (@{const_name "Trueprop"},_) $ (Const (@{const_name "op |"}, _) $ t $ _)) = rigid t
  44.161 +  | ok4horn (Const (@{const_name "Trueprop"},_) $ t) = rigid t
  44.162    | ok4horn _ = false;
  44.163  
  44.164  (*Create a meta-level Horn clause*)
  44.165 @@ -464,7 +464,7 @@
  44.166  
  44.167  (***** MESON PROOF PROCEDURE *****)
  44.168  
  44.169 -fun rhyps (Const("==>",_) $ (Const("Trueprop",_) $ A) $ phi,
  44.170 +fun rhyps (Const("==>",_) $ (Const(@{const_name "Trueprop"},_) $ A) $ phi,
  44.171             As) = rhyps(phi, A::As)
  44.172    | rhyps (_, As) = As;
  44.173  
  44.174 @@ -509,8 +509,8 @@
  44.175  val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,
  44.176                 not_impD, not_iffD, not_allD, not_exD, not_notD];
  44.177  
  44.178 -fun ok4nnf (Const ("Trueprop",_) $ (Const ("Not", _) $ t)) = rigid t
  44.179 -  | ok4nnf (Const ("Trueprop",_) $ t) = rigid t
  44.180 +fun ok4nnf (Const (@{const_name "Trueprop"},_) $ (Const (@{const_name "Not"}, _) $ t)) = rigid t
  44.181 +  | ok4nnf (Const (@{const_name "Trueprop"},_) $ t) = rigid t
  44.182    | ok4nnf _ = false;
  44.183  
  44.184  fun make_nnf1 ctxt th =
    45.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Thu Aug 19 10:27:12 2010 +0200
    45.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Thu Aug 19 11:02:14 2010 +0200
    45.3 @@ -676,7 +676,7 @@
    45.4          val T = ctyp_of_term c
    45.5          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
    45.6        in SOME (mk_meta_eq th) end
    45.7 -  | Const("op =",_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
    45.8 +  | Const(@{const_name "op ="},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
    45.9        let
   45.10          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
   45.11          val _ = map is_number [a,b,c]
   45.12 @@ -697,7 +697,7 @@
   45.13          val T = ctyp_of_term c
   45.14          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
   45.15        in SOME (mk_meta_eq th) end
   45.16 -  | Const("op =",_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
   45.17 +  | Const(@{const_name "op ="},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
   45.18      let
   45.19        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
   45.20          val _ = map is_number [a,b,c]
    46.1 --- a/src/HOL/Tools/prop_logic.ML	Thu Aug 19 10:27:12 2010 +0200
    46.2 +++ b/src/HOL/Tools/prop_logic.ML	Thu Aug 19 11:02:14 2010 +0200
    46.3 @@ -391,20 +391,20 @@
    46.4  				next_idx_is_valid := true;
    46.5  				Unsynchronized.inc next_idx
    46.6  			)
    46.7 -		fun aux (Const ("True", _))         table =
    46.8 +		fun aux (Const (@{const_name "True"}, _))         table =
    46.9  			(True, table)
   46.10 -		  | aux (Const ("False", _))        table =
   46.11 +		  | aux (Const (@{const_name "False"}, _))        table =
   46.12  			(False, table)
   46.13 -		  | aux (Const ("Not", _) $ x)      table =
   46.14 +		  | aux (Const (@{const_name "Not"}, _) $ x)      table =
   46.15  			apfst Not (aux x table)
   46.16 -		  | aux (Const ("op |", _) $ x $ y) table =
   46.17 +		  | aux (Const (@{const_name "op |"}, _) $ x $ y) table =
   46.18  			let
   46.19  				val (fm1, table1) = aux x table
   46.20  				val (fm2, table2) = aux y table1
   46.21  			in
   46.22  				(Or (fm1, fm2), table2)
   46.23  			end
   46.24 -		  | aux (Const ("op &", _) $ x $ y) table =
   46.25 +		  | aux (Const (@{const_name "op &"}, _) $ x $ y) table =
   46.26  			let
   46.27  				val (fm1, table1) = aux x table
   46.28  				val (fm2, table2) = aux y table1
    47.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Thu Aug 19 10:27:12 2010 +0200
    47.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Thu Aug 19 11:02:14 2010 +0200
    47.3 @@ -342,7 +342,7 @@
    47.4      val bound_max = length Ts - 1;
    47.5      val bounds = map_index (fn (i, ty) =>
    47.6        (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
    47.7 -    fun strip_imp (Const("op -->",_) $ A $ B) = apfst (cons A) (strip_imp B)
    47.8 +    fun strip_imp (Const(@{const_name "op -->"},_) $ A $ B) = apfst (cons A) (strip_imp B)
    47.9        | strip_imp A = ([], A)
   47.10      val prop' = betapplys (prop, map (fn (i, _, _, _) => Bound i) bounds);
   47.11      val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds)
    48.1 --- a/src/HOL/Tools/sat_funcs.ML	Thu Aug 19 10:27:12 2010 +0200
    48.2 +++ b/src/HOL/Tools/sat_funcs.ML	Thu Aug 19 11:02:14 2010 +0200
    48.3 @@ -217,7 +217,7 @@
    48.4  	(* Thm.cterm -> int option *)
    48.5  	fun index_of_literal chyp = (
    48.6  		case (HOLogic.dest_Trueprop o Thm.term_of) chyp of
    48.7 -		  (Const ("Not", _) $ atom) =>
    48.8 +		  (Const (@{const_name "Not"}, _) $ atom) =>
    48.9  			SOME (~ (the (Termtab.lookup atom_table atom)))
   48.10  		| atom =>
   48.11  			SOME (the (Termtab.lookup atom_table atom))
    49.1 --- a/src/HOL/ex/SVC_Oracle.thy	Thu Aug 19 10:27:12 2010 +0200
    49.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Thu Aug 19 11:02:14 2010 +0200
    49.3 @@ -88,18 +88,18 @@
    49.4              else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
    49.5              else replace (c $ x $ y)   (*non-numeric comparison*)
    49.6      (*abstraction of a formula*)
    49.7 -    and fm ((c as Const("op &", _)) $ p $ q) = c $ (fm p) $ (fm q)
    49.8 -      | fm ((c as Const("op |", _)) $ p $ q) = c $ (fm p) $ (fm q)
    49.9 -      | fm ((c as Const("op -->", _)) $ p $ q) = c $ (fm p) $ (fm q)
   49.10 -      | fm ((c as Const("Not", _)) $ p) = c $ (fm p)
   49.11 -      | fm ((c as Const("True", _))) = c
   49.12 -      | fm ((c as Const("False", _))) = c
   49.13 -      | fm (t as Const("op =",  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
   49.14 +    and fm ((c as Const(@{const_name "op &"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
   49.15 +      | fm ((c as Const(@{const_name "op |"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
   49.16 +      | fm ((c as Const(@{const_name "op -->"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
   49.17 +      | fm ((c as Const(@{const_name "Not"}, _)) $ p) = c $ (fm p)
   49.18 +      | fm ((c as Const(@{const_name "True"}, _))) = c
   49.19 +      | fm ((c as Const(@{const_name "False"}, _))) = c
   49.20 +      | fm (t as Const(@{const_name "op ="},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
   49.21        | fm (t as Const(@{const_name Orderings.less},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
   49.22        | fm (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
   49.23        | fm t = replace t
   49.24      (*entry point, and abstraction of a meta-formula*)
   49.25 -    fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)
   49.26 +    fun mt ((c as Const(@{const_name "Trueprop"}, _)) $ p) = c $ (fm p)
   49.27        | mt ((c as Const("==>", _)) $ p $ q)  = c $ (mt p) $ (mt q)
   49.28        | mt t = fm t  (*it might be a formula*)
   49.29    in (list_all (params, mt body), !pairs) end;
    50.1 --- a/src/HOL/ex/svc_funcs.ML	Thu Aug 19 10:27:12 2010 +0200
    50.2 +++ b/src/HOL/ex/svc_funcs.ML	Thu Aug 19 11:02:14 2010 +0200
    50.3 @@ -89,13 +89,13 @@
    50.4     let fun tag t =
    50.5           let val (c,ts) = strip_comb t
    50.6           in  case c of
    50.7 -             Const("op &", _)   => apply c (map tag ts)
    50.8 -           | Const("op |", _)   => apply c (map tag ts)
    50.9 -           | Const("op -->", _) => apply c (map tag ts)
   50.10 -           | Const("Not", _)    => apply c (map tag ts)
   50.11 -           | Const("True", _)   => (c, false)
   50.12 -           | Const("False", _)  => (c, false)
   50.13 -           | Const("op =", Type ("fun", [T,_])) =>
   50.14 +             Const(@{const_name "op &"}, _)   => apply c (map tag ts)
   50.15 +           | Const(@{const_name "op |"}, _)   => apply c (map tag ts)
   50.16 +           | Const(@{const_name "op -->"}, _) => apply c (map tag ts)
   50.17 +           | Const(@{const_name "Not"}, _)    => apply c (map tag ts)
   50.18 +           | Const(@{const_name "True"}, _)   => (c, false)
   50.19 +           | Const(@{const_name "False"}, _)  => (c, false)
   50.20 +           | Const(@{const_name "op ="}, Type ("fun", [T,_])) =>
   50.21                   if T = HOLogic.boolT then
   50.22                       (*biconditional: with int/nat comparisons below?*)
   50.23                       let val [t1,t2] = ts
   50.24 @@ -183,16 +183,16 @@
   50.25        | tm t = Int (lit t)
   50.26                 handle Match => var (t,[])
   50.27      (*translation of a formula*)
   50.28 -    and fm pos (Const("op &", _) $ p $ q) =
   50.29 +    and fm pos (Const(@{const_name "op &"}, _) $ p $ q) =
   50.30              Buildin("AND", [fm pos p, fm pos q])
   50.31 -      | fm pos (Const("op |", _) $ p $ q) =
   50.32 +      | fm pos (Const(@{const_name "op |"}, _) $ p $ q) =
   50.33              Buildin("OR", [fm pos p, fm pos q])
   50.34 -      | fm pos (Const("op -->", _) $ p $ q) =
   50.35 +      | fm pos (Const(@{const_name "op -->"}, _) $ p $ q) =
   50.36              Buildin("=>", [fm (not pos) p, fm pos q])
   50.37 -      | fm pos (Const("Not", _) $ p) =
   50.38 +      | fm pos (Const(@{const_name "Not"}, _) $ p) =
   50.39              Buildin("NOT", [fm (not pos) p])
   50.40 -      | fm pos (Const("True", _)) = TrueExpr
   50.41 -      | fm pos (Const("False", _)) = FalseExpr
   50.42 +      | fm pos (Const(@{const_name "True"}, _)) = TrueExpr
   50.43 +      | fm pos (Const(@{const_name "False"}, _)) = FalseExpr
   50.44        | fm pos (Const("SVC_Oracle.iff_keep", _) $ p $ q) =
   50.45               (*polarity doesn't matter*)
   50.46              Buildin("=", [fm pos p, fm pos q])
   50.47 @@ -200,7 +200,7 @@
   50.48              Buildin("AND",   (*unfolding uses both polarities*)
   50.49                           [Buildin("=>", [fm (not pos) p, fm pos q]),
   50.50                            Buildin("=>", [fm (not pos) q, fm pos p])])
   50.51 -      | fm pos (t as Const("op =", Type ("fun", [T,_])) $ x $ y) =
   50.52 +      | fm pos (t as Const(@{const_name "op ="}, Type ("fun", [T,_])) $ x $ y) =
   50.53              let val tx = tm x and ty = tm y
   50.54                  in if pos orelse T = HOLogic.realT then
   50.55                         Buildin("=", [tx, ty])
   50.56 @@ -225,7 +225,7 @@
   50.57              else fail t
   50.58        | fm pos t = var(t,[]);
   50.59        (*entry point, and translation of a meta-formula*)
   50.60 -      fun mt pos ((c as Const("Trueprop", _)) $ p) = fm pos (iff_tag p)
   50.61 +      fun mt pos ((c as Const(@{const_name "Trueprop"}, _)) $ p) = fm pos (iff_tag p)
   50.62          | mt pos ((c as Const("==>", _)) $ p $ q) =
   50.63              Buildin("=>", [mt (not pos) p, mt pos q])
   50.64          | mt pos t = fm pos (iff_tag t)  (*it might be a formula*)
    51.1 --- a/src/HOLCF/Tools/Domain/domain_library.ML	Thu Aug 19 10:27:12 2010 +0200
    51.2 +++ b/src/HOLCF/Tools/Domain/domain_library.ML	Thu Aug 19 11:02:14 2010 +0200
    51.3 @@ -121,8 +121,8 @@
    51.4        val r_inst = read_instantiate ctxt;
    51.5        fun at thm =
    51.6            case concl_of thm of
    51.7 -            _$(Const("op &",_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
    51.8 -          | _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec))
    51.9 +            _$(Const(@{const_name "op &"},_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
   51.10 +          | _$(Const(@{const_name "All"} ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec))
   51.11            | _                             => [thm];
   51.12      in map zero_var_indexes (at thm) end;
   51.13