tuned quotes
authorhaftmann
Thu Aug 19 16:08:59 2010 +0200 (2010-08-19)
changeset 3855832ad17fe2b9c
parent 38557 9926c47ad1a1
child 38559 befdd6833ec0
tuned quotes
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/Cooper.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/shuffler.ML
src/HOL/Library/Eval_Witness.thy
src/HOL/Library/positivstellensatz.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/Statespace/distinct_tree_prover.ML
src/HOL/Statespace/state_fun.ML
src/HOL/Statespace/state_space.ML
src/HOL/Tools/Function/function_core.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/Qelim/cooper.ML
src/HOL/Tools/Quotient/quotient_term.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/prop_logic.ML
src/HOL/Tools/sat_funcs.ML
src/HOL/Tools/simpdata.ML
src/HOL/ex/SVC_Oracle.thy
src/HOL/ex/svc_funcs.ML
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Thu Aug 19 16:08:54 2010 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Aug 19 16:08:59 2010 +0200
     1.3 @@ -3301,10 +3301,10 @@
     1.4  ML {*
     1.5    fun reorder_bounds_tac prems i =
     1.6      let
     1.7 -      fun variable_of_bound (Const (@{const_name "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 (@{const_name "Trueprop"}, _) $
    1.12 +        | variable_of_bound (Const (@{const_name Trueprop}, _) $
    1.13                               (Const (@{const_name "op ="}, _) $
    1.14                                Free (name, _) $ _)) = name
    1.15          | variable_of_bound t = raise TERM ("variable_of_bound", [t])
     2.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Thu Aug 19 16:08:54 2010 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Thu Aug 19 16:08:59 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 (@{const_name "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 (@{const_name "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/Ferrack.thy	Thu Aug 19 16:08:54 2010 +0200
     3.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Thu Aug 19 16:08:59 2010 +0200
     3.3 @@ -2000,9 +2000,9 @@
     3.4    | fm_of_term vs (@{term "op |"} $ t1 $ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
     3.5    | fm_of_term vs (@{term "op -->"} $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
     3.6    | fm_of_term vs (@{term "Not"} $ t') = @{code NOT} (fm_of_term vs t')
     3.7 -  | fm_of_term vs (Const (@{const_name "Ex"}, _) $ Abs (xn, xT, p)) =
     3.8 +  | fm_of_term vs (Const (@{const_name Ex}, _) $ Abs (xn, xT, p)) =
     3.9        @{code E} (fm_of_term (("", dummyT) :: vs) p)
    3.10 -  | fm_of_term vs (Const (@{const_name "All"}, _) $ Abs (xn, xT, p)) =
    3.11 +  | fm_of_term vs (Const (@{const_name All}, _) $ Abs (xn, xT, p)) =
    3.12        @{code A} (fm_of_term (("", dummyT) ::  vs) p)
    3.13    | fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t);
    3.14  
     4.1 --- a/src/HOL/Decision_Procs/MIR.thy	Thu Aug 19 16:08:54 2010 +0200
     4.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Thu Aug 19 16:08:59 2010 +0200
     4.3 @@ -5845,9 +5845,9 @@
     4.4        @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
     4.5    | fm_of_term vs (@{term "Not"} $ t') =
     4.6        @{code NOT} (fm_of_term vs t')
     4.7 -  | fm_of_term vs (Const (@{const_name "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 (map (fn (v, n) => (v, n + 1)) vs) p)
    4.10 -  | fm_of_term vs (Const (@{const_name "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 (map (fn (v, n) => (v, n + 1)) 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/Parametric_Ferrante_Rackoff.thy	Thu Aug 19 16:08:54 2010 +0200
     5.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Aug 19 16:08:59 2010 +0200
     5.3 @@ -3015,9 +3015,9 @@
     5.4  
     5.5  fun fm_of_term m m' fm = 
     5.6   case fm of
     5.7 -    Const(@{const_name "True"},_) => @{code T}
     5.8 -  | Const(@{const_name "False"},_) => @{code F}
     5.9 -  | Const(@{const_name "Not"},_)$p => @{code NOT} (fm_of_term m m' p)
    5.10 +    Const(@{const_name True},_) => @{code T}
    5.11 +  | Const(@{const_name False},_) => @{code F}
    5.12 +  | Const(@{const_name Not},_)$p => @{code NOT} (fm_of_term m m' p)
    5.13    | Const(@{const_name "op &"},_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
    5.14    | Const(@{const_name "op |"},_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
    5.15    | Const(@{const_name "op -->"},_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
    5.16 @@ -3028,13 +3028,13 @@
    5.17          @{code Lt} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
    5.18    | Const(@{const_name Orderings.less_eq},_)$p$q => 
    5.19          @{code Le} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
    5.20 -  | Const(@{const_name "Ex"},_)$Abs(xn,xT,p) => 
    5.21 +  | Const(@{const_name Ex},_)$Abs(xn,xT,p) => 
    5.22       let val (xn', p') =  variant_abs (xn,xT,p)
    5.23           val x = Free(xn',xT)
    5.24           fun incr i = i + 1
    5.25           val m0 = (x,0):: (map (apsnd incr) m)
    5.26        in @{code E} (fm_of_term m0 m' p') end
    5.27 -  | Const(@{const_name "All"},_)$Abs(xn,xT,p) => 
    5.28 +  | Const(@{const_name All},_)$Abs(xn,xT,p) => 
    5.29       let val (xn', p') =  variant_abs (xn,xT,p)
    5.30           val x = Free(xn',xT)
    5.31           fun incr i = i + 1
    5.32 @@ -3045,8 +3045,8 @@
    5.33  
    5.34  fun term_of_fm T m m' t = 
    5.35    case t of
    5.36 -    @{code T} => Const(@{const_name "True"},bT)
    5.37 -  | @{code F} => Const(@{const_name "False"},bT)
    5.38 +    @{code T} => Const(@{const_name True},bT)
    5.39 +  | @{code F} => Const(@{const_name False},bT)
    5.40    | @{code NOT} p => nott $ (term_of_fm T m m' p)
    5.41    | @{code And} (p,q) => conjt $ (term_of_fm T m m' p) $ (term_of_fm T m m' q)
    5.42    | @{code Or} (p,q) => disjt $ (term_of_fm T m m' p) $ (term_of_fm T m m' q)
     6.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Thu Aug 19 16:08:54 2010 +0200
     6.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Thu Aug 19 16:08:59 2010 +0200
     6.3 @@ -110,7 +110,7 @@
     6.4      fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
     6.5      (* The result of the quantifier elimination *)
     6.6      val (th, tac) = case (prop_of pre_thm) of
     6.7 -        Const ("==>", _) $ (Const (@{const_name "Trueprop"}, _) $ t1) $ _ =>
     6.8 +        Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
     6.9      let val pth = linzqe_oracle (cterm_of thy (Pattern.eta_long [] t1))
    6.10      in
    6.11            ((pth RS iffD2) RS pre_thm,
     7.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML	Thu Aug 19 16:08:54 2010 +0200
     7.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Thu Aug 19 16:08:59 2010 +0200
     7.3 @@ -91,7 +91,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 (@{const_name "Trueprop"}, _) $ t1) $ _ =>
     7.8 +        Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
     7.9      let val pth = linr_oracle (ctxt, Pattern.eta_long [] t1)
    7.10      in 
    7.11            (trace_msg ("calling procedure with term:\n" ^
     8.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Aug 19 16:08:54 2010 +0200
     8.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Aug 19 16:08:59 2010 +0200
     8.3 @@ -77,7 +77,7 @@
     8.4   fun main vs p =
     8.5    let
     8.6     val ((xn,ce),(x,fm)) = (case term_of p of
     8.7 -                   Const(@{const_name "Ex"},_)$Abs(xn,xT,_) =>
     8.8 +                   Const(@{const_name Ex},_)$Abs(xn,xT,_) =>
     8.9                          Thm.dest_comb p ||> Thm.dest_abs (SOME xn) |>> pair xn
    8.10                   | _ => raise CTERM ("main QE only treats existential quantifiers!", [p]))
    8.11     val cT = ctyp_of_term x
    8.12 @@ -178,16 +178,16 @@
    8.13       Const (@{const_name "op ="}, T) $ _ $ _ =>
    8.14         if domain_type T = HOLogic.boolT then find_args bounds tm
    8.15         else Thm.dest_fun2 tm
    8.16 -   | Const (@{const_name "Not"}, _) $ _ => h bounds (Thm.dest_arg tm)
    8.17 -   | Const (@{const_name "All"}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    8.18 -   | Const (@{const_name "Ex"}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    8.19 +   | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
    8.20 +   | Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    8.21 +   | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    8.22     | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
    8.23     | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
    8.24     | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
    8.25     | Const ("==>", _) $ _ $ _ => find_args bounds tm
    8.26     | Const ("==", _) $ _ $ _ => find_args bounds tm
    8.27     | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
    8.28 -   | Const (@{const_name "Trueprop"}, _) $ _ => h bounds (Thm.dest_arg tm)
    8.29 +   | Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm)
    8.30     | _ => Thm.dest_fun2 tm)
    8.31    and find_args bounds tm =
    8.32             (h bounds (Thm.dest_arg tm) handle CTERM _ => Thm.dest_arg1 tm)
     9.1 --- a/src/HOL/Decision_Procs/langford.ML	Thu Aug 19 16:08:54 2010 +0200
     9.2 +++ b/src/HOL/Decision_Procs/langford.ML	Thu Aug 19 16:08:59 2010 +0200
     9.3 @@ -30,7 +30,7 @@
     9.4  
     9.5  fun basic_dloqe ctxt stupid dlo_qeth dlo_qeth_nolb dlo_qeth_noub gather ep = 
     9.6   case term_of ep of 
     9.7 -  Const(@{const_name "Ex"},_)$_ => 
     9.8 +  Const(@{const_name Ex},_)$_ => 
     9.9     let 
    9.10       val p = Thm.dest_arg ep
    9.11       val ths = simplify (HOL_basic_ss addsimps gather) (instantiate' [] [SOME p] stupid)
    9.12 @@ -122,7 +122,7 @@
    9.13  local 
    9.14  fun proc ct = 
    9.15   case term_of ct of
    9.16 -  Const(@{const_name "Ex"},_)$Abs (xn,_,_) => 
    9.17 +  Const(@{const_name Ex},_)$Abs (xn,_,_) => 
    9.18     let 
    9.19      val e = Thm.dest_fun ct
    9.20      val (x,p) = Thm.dest_abs (SOME xn) (Thm.dest_arg ct)
    9.21 @@ -179,16 +179,16 @@
    9.22       Const (@{const_name "op ="}, T) $ _ $ _ =>
    9.23         if domain_type T = HOLogic.boolT then find_args bounds tm
    9.24         else Thm.dest_fun2 tm
    9.25 -   | Const (@{const_name "Not"}, _) $ _ => h bounds (Thm.dest_arg tm)
    9.26 -   | Const (@{const_name "All"}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    9.27 +   | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
    9.28 +   | Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    9.29     | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
    9.30 -   | Const (@{const_name "Ex"}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    9.31 +   | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    9.32     | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
    9.33     | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
    9.34     | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
    9.35     | Const ("==>", _) $ _ $ _ => find_args bounds tm
    9.36     | Const ("==", _) $ _ $ _ => find_args bounds tm
    9.37 -   | Const (@{const_name "Trueprop"}, _) $ _ => h bounds (Thm.dest_arg tm)
    9.38 +   | Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm)
    9.39     | _ => Thm.dest_fun2 tm)
    9.40    and find_args bounds tm =
    9.41      (h bounds (Thm.dest_arg tm) handle CTERM _ => h bounds (Thm.dest_arg1 tm))
    10.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Thu Aug 19 16:08:54 2010 +0200
    10.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Thu Aug 19 16:08:59 2010 +0200
    10.3 @@ -132,7 +132,7 @@
    10.4      fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
    10.5      (* The result of the quantifier elimination *)
    10.6      val (th, tac) = case (prop_of pre_thm) of
    10.7 -        Const ("==>", _) $ (Const (@{const_name "Trueprop"}, _) $ t1) $ _ =>
    10.8 +        Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
    10.9      let val pth =
   10.10            (* If quick_and_dirty then run without proof generation as oracle*)
   10.11               if !quick_and_dirty
    11.1 --- a/src/HOL/Import/shuffler.ML	Thu Aug 19 16:08:54 2010 +0200
    11.2 +++ b/src/HOL/Import/shuffler.ML	Thu Aug 19 16:08:59 2010 +0200
    11.3 @@ -60,14 +60,14 @@
    11.4  
    11.5  fun mk_meta_eq th =
    11.6      (case concl_of th of
    11.7 -         Const(@{const_name "Trueprop"},_) $ (Const(@{const_name "op ="},_) $ _ $ _) => th RS eq_reflection
    11.8 +         Const(@{const_name Trueprop},_) $ (Const(@{const_name "op ="},_) $ _ $ _) => th RS eq_reflection
    11.9         | Const("==",_) $ _ $ _ => th
   11.10         | _ => raise THM("Not an equality",0,[th]))
   11.11      handle _ => raise THM("Couldn't make meta equality",0,[th])  (* FIXME avoid handle _ *)
   11.12  
   11.13  fun mk_obj_eq th =
   11.14      (case concl_of th of
   11.15 -         Const(@{const_name "Trueprop"},_) $ (Const(@{const_name "op ="},_) $ _ $ _) => th
   11.16 +         Const(@{const_name Trueprop},_) $ (Const(@{const_name "op ="},_) $ _ $ _) => th
   11.17         | Const("==",_) $ _ $ _ => th RS meta_eq_to_obj_eq
   11.18         | _ => raise THM("Not an equality",0,[th]))
   11.19      handle _ => raise THM("Couldn't make object equality",0,[th])  (* FIXME avoid handle _ *)
    12.1 --- a/src/HOL/Library/Eval_Witness.thy	Thu Aug 19 16:08:54 2010 +0200
    12.2 +++ b/src/HOL/Library/Eval_Witness.thy	Thu Aug 19 16:08:59 2010 +0200
    12.3 @@ -63,7 +63,7 @@
    12.4      else error ("Type " ^ quote (Syntax.string_of_typ_global thy T) ^ " not allowed for ML witnesses")
    12.5  
    12.6    fun dest_exs  0 t = t
    12.7 -    | dest_exs n (Const (@{const_name "Ex"}, _) $ Abs (v,T,b)) = 
    12.8 +    | dest_exs n (Const (@{const_name Ex}, _) $ Abs (v,T,b)) = 
    12.9        Abs (v, check_type T, dest_exs (n - 1) b)
   12.10      | dest_exs _ _ = sys_error "dest_exs";
   12.11    val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
    13.1 --- a/src/HOL/Library/positivstellensatz.ML	Thu Aug 19 16:08:54 2010 +0200
    13.2 +++ b/src/HOL/Library/positivstellensatz.ML	Thu Aug 19 16:08:59 2010 +0200
    13.3 @@ -498,7 +498,7 @@
    13.4   val strip_exists =
    13.5    let fun h (acc, t) =
    13.6     case (term_of t) of
    13.7 -    Const(@{const_name "Ex"},_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
    13.8 +    Const(@{const_name Ex},_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
    13.9    | _ => (acc,t)
   13.10    in fn t => h ([],t)
   13.11    end
   13.12 @@ -515,7 +515,7 @@
   13.13   fun mk_ex v t = Thm.capply (ext (ctyp_of_term v)) (Thm.cabs v t)
   13.14  
   13.15   fun choose v th th' = case concl_of th of 
   13.16 -   @{term Trueprop} $ (Const(@{const_name "Ex"},_)$_) => 
   13.17 +   @{term Trueprop} $ (Const(@{const_name Ex},_)$_) => 
   13.18      let
   13.19       val p = (funpow 2 Thm.dest_arg o cprop_of) th
   13.20       val T = (hd o Thm.dest_ctyp o ctyp_of_term) p
   13.21 @@ -533,7 +533,7 @@
   13.22   val strip_forall =
   13.23    let fun h (acc, t) =
   13.24     case (term_of t) of
   13.25 -    Const(@{const_name "All"},_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
   13.26 +    Const(@{const_name All},_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
   13.27    | _ => (acc,t)
   13.28    in fn t => h ([],t)
   13.29    end
    14.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Thu Aug 19 16:08:54 2010 +0200
    14.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Thu Aug 19 16:08:59 2010 +0200
    14.3 @@ -183,7 +183,7 @@
    14.4    end;
    14.5  
    14.6  fun mk_not_sym ths = maps (fn th => case prop_of th of
    14.7 -    _ $ (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _)) => [th, th RS not_sym]
    14.8 +    _ $ (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _)) => [th, th RS not_sym]
    14.9    | _ => [th]) ths;
   14.10  
   14.11  fun fresh_const T U = Const ("Nominal.fresh", T --> U --> HOLogic.boolT);
   14.12 @@ -1372,7 +1372,7 @@
   14.13                              SUBGOAL (fn (t, i) => case Logic.strip_assums_concl t of
   14.14                                  _ $ (Const ("Nominal.fresh", _) $ _ $ _) =>
   14.15                                    simp_tac ind_ss1' i
   14.16 -                              | _ $ (Const (@{const_name "Not"}, _) $ _) =>
   14.17 +                              | _ $ (Const (@{const_name Not}, _) $ _) =>
   14.18                                    resolve_tac freshs2' i
   14.19                                | _ => asm_simp_tac (HOL_basic_ss addsimps
   14.20                                    pt2_atoms addsimprocs [perm_simproc]) i)) 1])
   14.21 @@ -1671,7 +1671,7 @@
   14.22      val rec_unique_frees' =
   14.23        Datatype_Prop.indexify_names (replicate (length recTs) "y") ~~ rec_result_Ts;
   14.24      val rec_unique_concls = map (fn ((x, U), R) =>
   14.25 -        Const (@{const_name "Ex1"}, (U --> HOLogic.boolT) --> HOLogic.boolT) $
   14.26 +        Const (@{const_name Ex1}, (U --> HOLogic.boolT) --> HOLogic.boolT) $
   14.27            Abs ("y", U, R $ Free x $ Bound 0))
   14.28        (rec_unique_frees ~~ rec_result_Ts ~~ rec_sets);
   14.29  
   14.30 @@ -1777,7 +1777,7 @@
   14.31                        | _ => false) prems';
   14.32                      val fresh_prems = filter (fn th => case prop_of th of
   14.33                          _ $ (Const ("Nominal.fresh", _) $ _ $ _) => true
   14.34 -                      | _ $ (Const (@{const_name "Not"}, _) $ _) => true
   14.35 +                      | _ $ (Const (@{const_name Not}, _) $ _) => true
   14.36                        | _ => false) prems';
   14.37                      val Ts = map fastype_of boundsl;
   14.38  
   14.39 @@ -1879,7 +1879,7 @@
   14.40                        end) rec_prems2;
   14.41  
   14.42                      val ihs = filter (fn th => case prop_of th of
   14.43 -                      _ $ (Const (@{const_name "All"}, _) $ _) => true | _ => false) prems';
   14.44 +                      _ $ (Const (@{const_name All}, _) $ _) => true | _ => false) prems';
   14.45  
   14.46                      (** pi1 o rs = pi2 o vs , rs = pi1^-1 o pi2 o vs **)
   14.47                      val _ = warning "step 7: pi1 o rs = pi2 o vs , rs = pi1^-1 o pi2 o vs";
   14.48 @@ -2022,7 +2022,7 @@
   14.49            (reccomb_names ~~ recTs ~~ rec_result_Ts))
   14.50        |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
   14.51            (Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
   14.52 -           Const (@{const_name "The"}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
   14.53 +           Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
   14.54               set $ Free ("x", T) $ Free ("y", T'))))))
   14.55                 (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts));
   14.56  
    15.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Thu Aug 19 16:08:54 2010 +0200
    15.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Aug 19 16:08:59 2010 +0200
    15.3 @@ -78,7 +78,7 @@
    15.4    | split_conj _ _ _ _ = NONE;
    15.5  
    15.6  fun strip_all [] t = t
    15.7 -  | strip_all (_ :: xs) (Const (@{const_name "All"}, _) $ Abs (s, T, t)) = strip_all xs t;
    15.8 +  | strip_all (_ :: xs) (Const (@{const_name All}, _) $ Abs (s, T, t)) = strip_all xs t;
    15.9  
   15.10  (*********************************************************************)
   15.11  (* maps  R ... & (ALL pi_1 ... pi_n z. P z (pi_1 o ... o pi_n o t))  *)
    16.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Thu Aug 19 16:08:54 2010 +0200
    16.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Thu Aug 19 16:08:59 2010 +0200
    16.3 @@ -82,7 +82,7 @@
    16.4    | split_conj _ _ _ _ = NONE;
    16.5  
    16.6  fun strip_all [] t = t
    16.7 -  | strip_all (_ :: xs) (Const (@{const_name "All"}, _) $ Abs (s, T, t)) = strip_all xs t;
    16.8 +  | strip_all (_ :: xs) (Const (@{const_name All}, _) $ Abs (s, T, t)) = strip_all xs t;
    16.9  
   16.10  (*********************************************************************)
   16.11  (* maps  R ... & (ALL pi_1 ... pi_n z. P z (pi_1 o ... o pi_n o t))  *)
    17.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML	Thu Aug 19 16:08:54 2010 +0200
    17.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML	Thu Aug 19 16:08:59 2010 +0200
    17.3 @@ -135,7 +135,7 @@
    17.4      val thy = Context.theory_of context
    17.5      val thms_to_be_added = (case (prop_of orig_thm) of
    17.6          (* case: eqvt-lemma is of the implicational form *)
    17.7 -        (Const("==>", _) $ (Const (@{const_name "Trueprop"},_) $ hyp) $ (Const (@{const_name "Trueprop"},_) $ concl)) =>
    17.8 +        (Const("==>", _) $ (Const (@{const_name Trueprop},_) $ hyp) $ (Const (@{const_name Trueprop},_) $ concl)) =>
    17.9            let
   17.10              val (pi,typi) = get_pi concl thy
   17.11            in
   17.12 @@ -147,7 +147,7 @@
   17.13               else raise EQVT_FORM "Type Implication"
   17.14            end
   17.15         (* case: eqvt-lemma is of the equational form *)
   17.16 -      | (Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, _) $
   17.17 +      | (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $
   17.18              (Const (@{const_name "perm"},typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
   17.19             (if (apply_pi lhs (pi,typi)) = rhs
   17.20                 then [orig_thm]
    18.1 --- a/src/HOL/Statespace/distinct_tree_prover.ML	Thu Aug 19 16:08:54 2010 +0200
    18.2 +++ b/src/HOL/Statespace/distinct_tree_prover.ML	Thu Aug 19 16:08:59 2010 +0200
    18.3 @@ -343,7 +343,7 @@
    18.4    end handle Option => NONE)
    18.5  
    18.6  fun distinctTree_tac names ctxt 
    18.7 -      (Const (@{const_name "Trueprop"},_) $ (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op ="}, _) $ x $ y)), i) =
    18.8 +      (Const (@{const_name Trueprop},_) $ (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, _) $ x $ y)), i) =
    18.9    (case get_fst_success (neq_x_y ctxt x y) names of
   18.10       SOME neq => rtac neq i
   18.11     | NONE => no_tac)
    19.1 --- a/src/HOL/Statespace/state_fun.ML	Thu Aug 19 16:08:54 2010 +0200
    19.2 +++ b/src/HOL/Statespace/state_fun.ML	Thu Aug 19 16:08:59 2010 +0200
    19.3 @@ -43,9 +43,9 @@
    19.4  val conj_True = thm "conj_True";
    19.5  val conj_cong = thm "conj_cong";
    19.6  
    19.7 -fun isFalse (Const (@{const_name "False"},_)) = true
    19.8 +fun isFalse (Const (@{const_name False},_)) = true
    19.9    | isFalse _ = false;
   19.10 -fun isTrue (Const (@{const_name "True"},_)) = true
   19.11 +fun isTrue (Const (@{const_name True},_)) = true
   19.12    | isTrue _ = false;
   19.13  
   19.14  in
   19.15 @@ -305,10 +305,10 @@
   19.16  
   19.17         in
   19.18           (case t of
   19.19 -           (Const (@{const_name "Ex"},Tex)$Abs(s,T,t)) =>
   19.20 +           (Const (@{const_name Ex},Tex)$Abs(s,T,t)) =>
   19.21               (let val (eq,eT,nT,swap) = mkeq (dest_sel_eq t) 0;
   19.22                    val prop = list_all ([("n",nT),("x",eT)],
   19.23 -                              Logic.mk_equals (Const (@{const_name "Ex"},Tex)$Abs(s,T,eq),
   19.24 +                              Logic.mk_equals (Const (@{const_name Ex},Tex)$Abs(s,T,eq),
   19.25                                                 HOLogic.true_const));
   19.26                    val thm = Drule.export_without_context (prove prop);
   19.27                    val thm' = if swap then swap_ex_eq OF [thm] else thm
   19.28 @@ -367,7 +367,7 @@
   19.29       val (lookup_ss,ex_lookup_ss,simprocs_active) = StateFunData.get ctxt;
   19.30       val (lookup_ss', ex_lookup_ss') = 
   19.31             (case (concl_of thm) of
   19.32 -            (_$((Const (@{const_name "Ex"},_)$_))) => (lookup_ss, ex_lookup_ss addsimps [thm])
   19.33 +            (_$((Const (@{const_name Ex},_)$_))) => (lookup_ss, ex_lookup_ss addsimps [thm])
   19.34              | _ => (lookup_ss addsimps [thm], ex_lookup_ss))
   19.35       fun activate_simprocs ctxt =
   19.36            if simprocs_active then ctxt
    20.1 --- a/src/HOL/Statespace/state_space.ML	Thu Aug 19 16:08:54 2010 +0200
    20.2 +++ b/src/HOL/Statespace/state_space.ML	Thu Aug 19 16:08:59 2010 +0200
    20.3 @@ -222,8 +222,8 @@
    20.4    end handle Option => NONE)
    20.5  
    20.6  fun distinctTree_tac ctxt
    20.7 -      (Const (@{const_name "Trueprop"},_) $
    20.8 -        (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op ="}, _) $ (x as Free _)$ (y as Free _))), i) =
    20.9 +      (Const (@{const_name Trueprop},_) $
   20.10 +        (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, _) $ (x as Free _)$ (y as Free _))), i) =
   20.11    (case (neq_x_y ctxt x y) of
   20.12       SOME neq => rtac neq i
   20.13     | NONE => no_tac)
    21.1 --- a/src/HOL/Tools/Function/function_core.ML	Thu Aug 19 16:08:54 2010 +0200
    21.2 +++ b/src/HOL/Tools/Function/function_core.ML	Thu Aug 19 16:08:59 2010 +0200
    21.3 @@ -392,7 +392,7 @@
    21.4      (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
    21.5      val ihyp = Term.all domT $ Abs ("z", domT,
    21.6        Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
    21.7 -        HOLogic.mk_Trueprop (Const (@{const_name "Ex1"}, (ranT --> boolT) --> boolT) $
    21.8 +        HOLogic.mk_Trueprop (Const (@{const_name Ex1}, (ranT --> boolT) --> boolT) $
    21.9            Abs ("y", ranT, G $ Bound 1 $ Bound 0))))
   21.10        |> cterm_of thy
   21.11  
    22.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Aug 19 16:08:54 2010 +0200
    22.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Aug 19 16:08:59 2010 +0200
    22.3 @@ -147,7 +147,7 @@
    22.4  
    22.5  fun Trueprop_conv cv ct =
    22.6    case Thm.term_of ct of
    22.7 -    Const (@{const_name "Trueprop"}, _) $ _ => Conv.arg_conv cv ct  
    22.8 +    Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct  
    22.9    | _ => raise Fail "Trueprop_conv"
   22.10  
   22.11  fun preprocess_intro thy rule =
    23.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Aug 19 16:08:54 2010 +0200
    23.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Aug 19 16:08:59 2010 +0200
    23.3 @@ -411,7 +411,7 @@
    23.4  fun conjuncts t = conjuncts_aux t [];
    23.5  
    23.6  fun is_equationlike_term (Const ("==", _) $ _ $ _) = true
    23.7 -  | is_equationlike_term (Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _)) = true
    23.8 +  | is_equationlike_term (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _)) = true
    23.9    | is_equationlike_term _ = false
   23.10    
   23.11  val is_equationlike = is_equationlike_term o prop_of 
   23.12 @@ -479,7 +479,7 @@
   23.13  
   23.14  fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t)
   23.15  
   23.16 -fun strip_ex (Const (@{const_name "Ex"}, _) $ Abs (x, T, t)) =
   23.17 +fun strip_ex (Const (@{const_name Ex}, _) $ Abs (x, T, t)) =
   23.18    let
   23.19      val (xTs, t') = strip_ex t
   23.20    in
    24.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Aug 19 16:08:54 2010 +0200
    24.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Aug 19 16:08:59 2010 +0200
    24.3 @@ -576,7 +576,7 @@
    24.4  
    24.5  fun Trueprop_conv cv ct =
    24.6    case Thm.term_of ct of
    24.7 -    Const (@{const_name "Trueprop"}, _) $ _ => Conv.arg_conv cv ct  
    24.8 +    Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct  
    24.9    | _ => raise Fail "Trueprop_conv"
   24.10  
   24.11  fun preprocess_intro thy rule =
   24.12 @@ -587,7 +587,7 @@
   24.13  
   24.14  fun preprocess_elim ctxt elimrule =
   24.15    let
   24.16 -    fun replace_eqs (Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, T) $ lhs $ rhs)) =
   24.17 +    fun replace_eqs (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, T) $ lhs $ rhs)) =
   24.18         HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
   24.19       | replace_eqs t = t
   24.20      val thy = ProofContext.theory_of ctxt
    25.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu Aug 19 16:08:54 2010 +0200
    25.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu Aug 19 16:08:59 2010 +0200
    25.3 @@ -111,7 +111,7 @@
    25.4  
    25.5  fun mk_meta_equation th =
    25.6    case prop_of th of
    25.7 -    Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _) => th RS @{thm eq_reflection}
    25.8 +    Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _) => th RS @{thm eq_reflection}
    25.9    | _ => th
   25.10  
   25.11  val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp}
   25.12 @@ -215,12 +215,12 @@
   25.13  val logic_operator_names =
   25.14    [@{const_name "=="}, 
   25.15     @{const_name "==>"},
   25.16 -   @{const_name "Trueprop"},
   25.17 -   @{const_name "Not"},
   25.18 +   @{const_name Trueprop},
   25.19 +   @{const_name Not},
   25.20     @{const_name "op ="},
   25.21     @{const_name "op -->"},
   25.22 -   @{const_name "All"},
   25.23 -   @{const_name "Ex"}, 
   25.24 +   @{const_name All},
   25.25 +   @{const_name Ex}, 
   25.26     @{const_name "op &"},
   25.27     @{const_name "op |"}]
   25.28  
    26.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Thu Aug 19 16:08:54 2010 +0200
    26.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Thu Aug 19 16:08:59 2010 +0200
    26.3 @@ -86,9 +86,9 @@
    26.4     map instantiate rew_ths
    26.5   end
    26.6  
    26.7 -fun is_compound ((Const (@{const_name "Not"}, _)) $ t) =
    26.8 +fun is_compound ((Const (@{const_name Not}, _)) $ t) =
    26.9      error "is_compound: Negation should not occur; preprocessing is defect"
   26.10 -  | is_compound ((Const (@{const_name "Ex"}, _)) $ _) = true
   26.11 +  | is_compound ((Const (@{const_name Ex}, _)) $ _) = true
   26.12    | is_compound ((Const (@{const_name "op |"}, _)) $ _ $ _) = true
   26.13    | is_compound ((Const (@{const_name "op &"}, _)) $ _ $ _) =
   26.14      error "is_compound: Conjunction should not occur; preprocessing is defect"
    27.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Thu Aug 19 16:08:54 2010 +0200
    27.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Thu Aug 19 16:08:59 2010 +0200
    27.3 @@ -622,9 +622,9 @@
    27.4        Proc.Iff (fm_of_term ps vs t1, fm_of_term ps vs t2)
    27.5    | fm_of_term ps vs (Const (@{const_name Not}, _) $ t') =
    27.6        Proc.Not (fm_of_term ps vs t')
    27.7 -  | fm_of_term ps vs (Const (@{const_name "Ex"}, _) $ Abs abs) =
    27.8 +  | fm_of_term ps vs (Const (@{const_name Ex}, _) $ Abs abs) =
    27.9        Proc.E (uncurry (fm_of_term ps) (descend vs abs))
   27.10 -  | fm_of_term ps vs (Const (@{const_name "All"}, _) $ Abs abs) =
   27.11 +  | fm_of_term ps vs (Const (@{const_name All}, _) $ Abs abs) =
   27.12        Proc.A (uncurry (fm_of_term ps) (descend vs abs))
   27.13    | fm_of_term ps vs (@{term "op = :: int => _"} $ t1 $ t2) =
   27.14        Proc.Eq (Proc.Sub (num_of_term vs t1, num_of_term vs t2))
   27.15 @@ -694,7 +694,7 @@
   27.16  
   27.17  fun strip_objall ct = 
   27.18   case term_of ct of 
   27.19 -  Const (@{const_name "All"}, _) $ Abs (xn,xT,p) => 
   27.20 +  Const (@{const_name All}, _) $ Abs (xn,xT,p) => 
   27.21     let val (a,(v,t')) = (apsnd (Thm.dest_abs (SOME xn)) o Thm.dest_comb) ct
   27.22     in apfst (cons (a,v)) (strip_objall t')
   27.23     end
    28.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Thu Aug 19 16:08:54 2010 +0200
    28.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Thu Aug 19 16:08:59 2010 +0200
    28.3 @@ -490,16 +490,16 @@
    28.4           else mk_bex1_rel $ resrel $ subtrm
    28.5         end
    28.6  
    28.7 -  | (Const (@{const_name "Ex1"}, ty) $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
    28.8 +  | (Const (@{const_name Ex1}, ty) $ t, Const (@{const_name Ex1}, ty') $ t') =>
    28.9         let
   28.10           val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   28.11         in
   28.12 -         if ty = ty' then Const (@{const_name "Ex1"}, ty) $ subtrm
   28.13 +         if ty = ty' then Const (@{const_name Ex1}, ty) $ subtrm
   28.14           else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
   28.15         end
   28.16  
   28.17    | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
   28.18 -     Const (@{const_name "All"}, ty') $ t') =>
   28.19 +     Const (@{const_name All}, ty') $ t') =>
   28.20         let
   28.21           val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   28.22           val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
   28.23 @@ -510,7 +510,7 @@
   28.24         end
   28.25  
   28.26    | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
   28.27 -     Const (@{const_name "Ex"}, ty') $ t') =>
   28.28 +     Const (@{const_name Ex}, ty') $ t') =>
   28.29         let
   28.30           val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   28.31           val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
   28.32 @@ -520,7 +520,7 @@
   28.33           else mk_bex $ (mk_resp $ resrel) $ subtrm
   28.34         end
   28.35  
   28.36 -  | (Const (@{const_name "Bex1_rel"}, ty) $ resrel $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
   28.37 +  | (Const (@{const_name "Bex1_rel"}, ty) $ resrel $ t, Const (@{const_name Ex1}, ty') $ t') =>
   28.38         let
   28.39           val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   28.40           val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
   28.41 @@ -638,10 +638,10 @@
   28.42     as the type of subterms needs to be calculated   *)
   28.43  fun inj_repabs_trm ctxt (rtrm, qtrm) =
   28.44   case (rtrm, qtrm) of
   28.45 -    (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
   28.46 +    (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name All}, _) $ t') =>
   28.47         Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
   28.48  
   28.49 -  | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
   28.50 +  | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name Ex}, _) $ t') =>
   28.51         Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
   28.52  
   28.53    | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) =>
    29.1 --- a/src/HOL/Tools/choice_specification.ML	Thu Aug 19 16:08:54 2010 +0200
    29.2 +++ b/src/HOL/Tools/choice_specification.ML	Thu Aug 19 16:08:59 2010 +0200
    29.3 @@ -24,7 +24,7 @@
    29.4      fun mk_definitional [] arg = arg
    29.5        | mk_definitional ((thname,cname,covld)::cos) (thy,thm) =
    29.6          case HOLogic.dest_Trueprop (concl_of thm) of
    29.7 -            Const(@{const_name "Ex"},_) $ P =>
    29.8 +            Const(@{const_name Ex},_) $ P =>
    29.9              let
   29.10                  val ctype = domain_type (type_of P)
   29.11                  val cname_full = Sign.intern_const thy cname
   29.12 @@ -51,7 +51,7 @@
   29.13                  end
   29.14                | process ((thname,cname,covld)::cos) (thy,tm) =
   29.15                  case tm of
   29.16 -                    Const(@{const_name "Ex"},_) $ P =>
   29.17 +                    Const(@{const_name Ex},_) $ P =>
   29.18                      let
   29.19                          val ctype = domain_type (type_of P)
   29.20                          val cname_full = Sign.intern_const thy cname
    30.1 --- a/src/HOL/Tools/cnf_funcs.ML	Thu Aug 19 16:08:54 2010 +0200
    30.2 +++ b/src/HOL/Tools/cnf_funcs.ML	Thu Aug 19 16:08:59 2010 +0200
    30.3 @@ -93,16 +93,16 @@
    30.4  
    30.5  val cnftac_eq_imp        = @{lemma "[| P = Q; P |] ==> Q" by auto};
    30.6  
    30.7 -fun is_atom (Const (@{const_name "False"}, _))                                           = false
    30.8 -  | is_atom (Const (@{const_name "True"}, _))                                            = false
    30.9 +fun is_atom (Const (@{const_name False}, _))                                           = false
   30.10 +  | is_atom (Const (@{const_name True}, _))                                            = false
   30.11    | is_atom (Const (@{const_name "op &"}, _) $ _ $ _)                                    = false
   30.12    | is_atom (Const (@{const_name "op |"}, _) $ _ $ _)                                    = false
   30.13    | is_atom (Const (@{const_name "op -->"}, _) $ _ $ _)                                  = false
   30.14    | is_atom (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ _ $ _)       = false
   30.15 -  | is_atom (Const (@{const_name "Not"}, _) $ _)                                         = false
   30.16 +  | is_atom (Const (@{const_name Not}, _) $ _)                                         = false
   30.17    | is_atom _                                                              = true;
   30.18  
   30.19 -fun is_literal (Const (@{const_name "Not"}, _) $ x) = is_atom x
   30.20 +fun is_literal (Const (@{const_name Not}, _) $ x) = is_atom x
   30.21    | is_literal x                      = is_atom x;
   30.22  
   30.23  fun is_clause (Const (@{const_name "op |"}, _) $ x $ y) = is_clause x andalso is_clause y
   30.24 @@ -118,7 +118,7 @@
   30.25  fun clause_is_trivial c =
   30.26  	let
   30.27  		(* Term.term -> Term.term *)
   30.28 -		fun dual (Const (@{const_name "Not"}, _) $ x) = x
   30.29 +		fun dual (Const (@{const_name Not}, _) $ x) = x
   30.30  		  | dual x                      = HOLogic.Not $ x
   30.31  		(* Term.term list -> bool *)
   30.32  		fun has_duals []      = false
   30.33 @@ -214,32 +214,32 @@
   30.34  	in
   30.35  		make_nnf_iff OF [thm1, thm2, thm3, thm4]
   30.36  	end
   30.37 -  | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ Const (@{const_name "False"}, _)) =
   30.38 +  | make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name False}, _)) =
   30.39  	make_nnf_not_false
   30.40 -  | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ Const (@{const_name "True"}, _)) =
   30.41 +  | make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name True}, _)) =
   30.42  	make_nnf_not_true
   30.43 -  | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op &"}, _) $ x $ y)) =
   30.44 +  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op &"}, _) $ x $ y)) =
   30.45  	let
   30.46  		val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
   30.47  		val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
   30.48  	in
   30.49  		make_nnf_not_conj OF [thm1, thm2]
   30.50  	end
   30.51 -  | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op |"}, _) $ x $ y)) =
   30.52 +  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op |"}, _) $ x $ y)) =
   30.53  	let
   30.54  		val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
   30.55  		val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
   30.56  	in
   30.57  		make_nnf_not_disj OF [thm1, thm2]
   30.58  	end
   30.59 -  | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op -->"}, _) $ x $ y)) =
   30.60 +  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op -->"}, _) $ x $ y)) =
   30.61  	let
   30.62  		val thm1 = make_nnf_thm thy x
   30.63  		val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
   30.64  	in
   30.65  		make_nnf_not_imp OF [thm1, thm2]
   30.66  	end
   30.67 -  | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ x $ y)) =
   30.68 +  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ x $ y)) =
   30.69  	let
   30.70  		val thm1 = make_nnf_thm thy x
   30.71  		val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
   30.72 @@ -248,7 +248,7 @@
   30.73  	in
   30.74  		make_nnf_not_iff OF [thm1, thm2, thm3, thm4]
   30.75  	end
   30.76 -  | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "Not"}, _) $ x)) =
   30.77 +  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name Not}, _) $ x)) =
   30.78  	let
   30.79  		val thm1 = make_nnf_thm thy x
   30.80  	in
   30.81 @@ -430,7 +430,7 @@
   30.82  				in
   30.83  					make_cnf_disj_conj_r OF [thm1, thm2]  (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
   30.84  				end
   30.85 -			  | make_cnfx_disj_thm (Const (@{const_name "Ex"}, _) $ x') y' =
   30.86 +			  | make_cnfx_disj_thm (Const (@{const_name Ex}, _) $ x') y' =
   30.87  				let
   30.88  					val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_l   (* ((Ex x') | y') = (Ex (x' | y')) *)
   30.89  					val var  = new_free ()
   30.90 @@ -441,7 +441,7 @@
   30.91  				in
   30.92  					iff_trans OF [thm1, thm5]  (* ((Ex x') | y') = (Ex v. body') *)
   30.93  				end
   30.94 -			  | make_cnfx_disj_thm x' (Const (@{const_name "Ex"}, _) $ y') =
   30.95 +			  | make_cnfx_disj_thm x' (Const (@{const_name Ex}, _) $ y') =
   30.96  				let
   30.97  					val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_r   (* (x' | (Ex y')) = (Ex (x' | y')) *)
   30.98  					val var  = new_free ()
    31.1 --- a/src/HOL/Tools/groebner.ML	Thu Aug 19 16:08:54 2010 +0200
    31.2 +++ b/src/HOL/Tools/groebner.ML	Thu Aug 19 16:08:59 2010 +0200
    31.3 @@ -405,7 +405,7 @@
    31.4  val mk_comb = capply;
    31.5  fun is_neg t =
    31.6      case term_of t of
    31.7 -      (Const(@{const_name "Not"},_)$p) => true
    31.8 +      (Const(@{const_name Not},_)$p) => true
    31.9      | _  => false;
   31.10  fun is_eq t =
   31.11   case term_of t of
   31.12 @@ -430,14 +430,14 @@
   31.13  val strip_exists =
   31.14   let fun h (acc, t) =
   31.15        case (term_of t) of
   31.16 -       Const(@{const_name "Ex"},_)$Abs(x,T,p) => h (dest_abs NONE (dest_arg t) |>> (fn v => v::acc))
   31.17 +       Const(@{const_name Ex},_)$Abs(x,T,p) => h (dest_abs NONE (dest_arg t) |>> (fn v => v::acc))
   31.18       | _ => (acc,t)
   31.19   in fn t => h ([],t)
   31.20   end;
   31.21  
   31.22  fun is_forall t =
   31.23   case term_of t of
   31.24 -  (Const(@{const_name "All"},_)$Abs(_,_,_)) => true
   31.25 +  (Const(@{const_name All},_)$Abs(_,_,_)) => true
   31.26  | _ => false;
   31.27  
   31.28  val mk_object_eq = fn th => th COMP meta_eq_to_obj_eq;
   31.29 @@ -522,7 +522,7 @@
   31.30   fun mk_ex v t = Thm.capply (ext (ctyp_of_term v)) (Thm.cabs v t)
   31.31  
   31.32  fun choose v th th' = case concl_of th of 
   31.33 -  @{term Trueprop} $ (Const(@{const_name "Ex"},_)$_) => 
   31.34 +  @{term Trueprop} $ (Const(@{const_name Ex},_)$_) => 
   31.35     let
   31.36      val p = (funpow 2 Thm.dest_arg o cprop_of) th
   31.37      val T = (hd o Thm.dest_ctyp o ctyp_of_term) p
   31.38 @@ -926,9 +926,9 @@
   31.39      Const (@{const_name "op ="}, T) $ _ $ _ =>
   31.40        if domain_type T = HOLogic.boolT then find_args bounds tm
   31.41        else dest_arg tm
   31.42 -  | Const (@{const_name "Not"}, _) $ _ => find_term bounds (dest_arg tm)
   31.43 -  | Const (@{const_name "All"}, _) $ _ => find_body bounds (dest_arg tm)
   31.44 -  | Const (@{const_name "Ex"}, _) $ _ => find_body bounds (dest_arg tm)
   31.45 +  | Const (@{const_name Not}, _) $ _ => find_term bounds (dest_arg tm)
   31.46 +  | Const (@{const_name All}, _) $ _ => find_body bounds (dest_arg tm)
   31.47 +  | Const (@{const_name Ex}, _) $ _ => find_body bounds (dest_arg tm)
   31.48    | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
   31.49    | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
   31.50    | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
    32.1 --- a/src/HOL/Tools/lin_arith.ML	Thu Aug 19 16:08:54 2010 +0200
    32.2 +++ b/src/HOL/Tools/lin_arith.ML	Thu Aug 19 16:08:59 2010 +0200
    32.3 @@ -46,12 +46,12 @@
    32.4  val mk_Trueprop = HOLogic.mk_Trueprop;
    32.5  
    32.6  fun atomize thm = case Thm.prop_of thm of
    32.7 -    Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op &"}, _) $ _ $ _) =>
    32.8 +    Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op &"}, _) $ _ $ _) =>
    32.9      atomize (thm RS conjunct1) @ atomize (thm RS conjunct2)
   32.10    | _ => [thm];
   32.11  
   32.12 -fun neg_prop ((TP as Const(@{const_name "Trueprop"}, _)) $ (Const (@{const_name Not}, _) $ t)) = TP $ t
   32.13 -  | neg_prop ((TP as Const(@{const_name "Trueprop"}, _)) $ t) = TP $ (HOLogic.Not $t)
   32.14 +fun neg_prop ((TP as Const(@{const_name Trueprop}, _)) $ (Const (@{const_name Not}, _) $ t)) = TP $ t
   32.15 +  | neg_prop ((TP as Const(@{const_name Trueprop}, _)) $ t) = TP $ (HOLogic.Not $t)
   32.16    | neg_prop t = raise TERM ("neg_prop", [t]);
   32.17  
   32.18  fun is_False thm =
   32.19 @@ -258,10 +258,10 @@
   32.20    | negate NONE                        = NONE;
   32.21  
   32.22  fun decomp_negation data
   32.23 -  ((Const (@{const_name "Trueprop"}, _)) $ (Const (rel, T) $ lhs $ rhs)) : decomp option =
   32.24 +  ((Const (@{const_name Trueprop}, _)) $ (Const (rel, T) $ lhs $ rhs)) : decomp option =
   32.25        decomp_typecheck data (T, (rel, lhs, rhs))
   32.26 -  | decomp_negation data ((Const (@{const_name "Trueprop"}, _)) $
   32.27 -  (Const (@{const_name "Not"}, _) $ (Const (rel, T) $ lhs $ rhs))) =
   32.28 +  | decomp_negation data ((Const (@{const_name Trueprop}, _)) $
   32.29 +  (Const (@{const_name Not}, _) $ (Const (rel, T) $ lhs $ rhs))) =
   32.30        negate (decomp_typecheck data (T, (rel, lhs, rhs)))
   32.31    | decomp_negation data _ =
   32.32        NONE;
   32.33 @@ -273,7 +273,7 @@
   32.34    in decomp_negation (thy, discrete, inj_consts) end;
   32.35  
   32.36  fun domain_is_nat (_ $ (Const (_, T) $ _ $ _))                      = nT T
   32.37 -  | domain_is_nat (_ $ (Const (@{const_name "Not"}, _) $ (Const (_, T) $ _ $ _))) = nT T
   32.38 +  | domain_is_nat (_ $ (Const (@{const_name Not}, _) $ (Const (_, T) $ _ $ _))) = nT T
   32.39    | domain_is_nat _                                                 = false;
   32.40  
   32.41  
   32.42 @@ -659,7 +659,7 @@
   32.43  
   32.44  fun negated_term_occurs_positively (terms : term list) : bool =
   32.45    List.exists
   32.46 -    (fn (Trueprop $ (Const (@{const_name "Not"}, _) $ t)) =>
   32.47 +    (fn (Trueprop $ (Const (@{const_name Not}, _) $ t)) =>
   32.48        member Pattern.aeconv terms (Trueprop $ t)
   32.49        | _ => false)
   32.50      terms;
    33.1 --- a/src/HOL/Tools/prop_logic.ML	Thu Aug 19 16:08:54 2010 +0200
    33.2 +++ b/src/HOL/Tools/prop_logic.ML	Thu Aug 19 16:08:59 2010 +0200
    33.3 @@ -391,11 +391,11 @@
    33.4  				next_idx_is_valid := true;
    33.5  				Unsynchronized.inc next_idx
    33.6  			)
    33.7 -		fun aux (Const (@{const_name "True"}, _))         table =
    33.8 +		fun aux (Const (@{const_name True}, _))         table =
    33.9  			(True, table)
   33.10 -		  | aux (Const (@{const_name "False"}, _))        table =
   33.11 +		  | aux (Const (@{const_name False}, _))        table =
   33.12  			(False, table)
   33.13 -		  | aux (Const (@{const_name "Not"}, _) $ x)      table =
   33.14 +		  | aux (Const (@{const_name Not}, _) $ x)      table =
   33.15  			apfst Not (aux x table)
   33.16  		  | aux (Const (@{const_name "op |"}, _) $ x $ y) table =
   33.17  			let
    34.1 --- a/src/HOL/Tools/sat_funcs.ML	Thu Aug 19 16:08:54 2010 +0200
    34.2 +++ b/src/HOL/Tools/sat_funcs.ML	Thu Aug 19 16:08:59 2010 +0200
    34.3 @@ -217,7 +217,7 @@
    34.4  	(* Thm.cterm -> int option *)
    34.5  	fun index_of_literal chyp = (
    34.6  		case (HOLogic.dest_Trueprop o Thm.term_of) chyp of
    34.7 -		  (Const (@{const_name "Not"}, _) $ atom) =>
    34.8 +		  (Const (@{const_name Not}, _) $ atom) =>
    34.9  			SOME (~ (the (Termtab.lookup atom_table atom)))
   34.10  		| atom =>
   34.11  			SOME (the (Termtab.lookup atom_table atom))
    35.1 --- a/src/HOL/Tools/simpdata.ML	Thu Aug 19 16:08:54 2010 +0200
    35.2 +++ b/src/HOL/Tools/simpdata.ML	Thu Aug 19 16:08:59 2010 +0200
    35.3 @@ -45,7 +45,7 @@
    35.4    (*expects Trueprop if not == *)
    35.5    of Const (@{const_name "=="},_) $ _ $ _ => th
    35.6     | _ $ (Const (@{const_name "op ="}, _) $ _ $ _) => mk_meta_eq th
    35.7 -   | _ $ (Const (@{const_name "Not"}, _) $ _) => th RS @{thm Eq_FalseI}
    35.8 +   | _ $ (Const (@{const_name Not}, _) $ _) => th RS @{thm Eq_FalseI}
    35.9     | _ => th RS @{thm Eq_TrueI}
   35.10  
   35.11  fun mk_eq_True (_: simpset) r =
    36.1 --- a/src/HOL/ex/SVC_Oracle.thy	Thu Aug 19 16:08:54 2010 +0200
    36.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Thu Aug 19 16:08:59 2010 +0200
    36.3 @@ -91,15 +91,15 @@
    36.4      and fm ((c as Const(@{const_name "op &"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
    36.5        | fm ((c as Const(@{const_name "op |"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
    36.6        | fm ((c as Const(@{const_name "op -->"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
    36.7 -      | fm ((c as Const(@{const_name "Not"}, _)) $ p) = c $ (fm p)
    36.8 -      | fm ((c as Const(@{const_name "True"}, _))) = c
    36.9 -      | fm ((c as Const(@{const_name "False"}, _))) = c
   36.10 +      | fm ((c as Const(@{const_name Not}, _)) $ p) = c $ (fm p)
   36.11 +      | fm ((c as Const(@{const_name True}, _))) = c
   36.12 +      | fm ((c as Const(@{const_name False}, _))) = c
   36.13        | fm (t as Const(@{const_name "op ="},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
   36.14        | fm (t as Const(@{const_name Orderings.less},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
   36.15        | fm (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
   36.16        | fm t = replace t
   36.17      (*entry point, and abstraction of a meta-formula*)
   36.18 -    fun mt ((c as Const(@{const_name "Trueprop"}, _)) $ p) = c $ (fm p)
   36.19 +    fun mt ((c as Const(@{const_name Trueprop}, _)) $ p) = c $ (fm p)
   36.20        | mt ((c as Const("==>", _)) $ p $ q)  = c $ (mt p) $ (mt q)
   36.21        | mt t = fm t  (*it might be a formula*)
   36.22    in (list_all (params, mt body), !pairs) end;
    37.1 --- a/src/HOL/ex/svc_funcs.ML	Thu Aug 19 16:08:54 2010 +0200
    37.2 +++ b/src/HOL/ex/svc_funcs.ML	Thu Aug 19 16:08:59 2010 +0200
    37.3 @@ -92,9 +92,9 @@
    37.4               Const(@{const_name "op &"}, _)   => apply c (map tag ts)
    37.5             | Const(@{const_name "op |"}, _)   => apply c (map tag ts)
    37.6             | Const(@{const_name "op -->"}, _) => apply c (map tag ts)
    37.7 -           | Const(@{const_name "Not"}, _)    => apply c (map tag ts)
    37.8 -           | Const(@{const_name "True"}, _)   => (c, false)
    37.9 -           | Const(@{const_name "False"}, _)  => (c, false)
   37.10 +           | Const(@{const_name Not}, _)    => apply c (map tag ts)
   37.11 +           | Const(@{const_name True}, _)   => (c, false)
   37.12 +           | Const(@{const_name False}, _)  => (c, false)
   37.13             | Const(@{const_name "op ="}, Type ("fun", [T,_])) =>
   37.14                   if T = HOLogic.boolT then
   37.15                       (*biconditional: with int/nat comparisons below?*)
   37.16 @@ -189,10 +189,10 @@
   37.17              Buildin("OR", [fm pos p, fm pos q])
   37.18        | fm pos (Const(@{const_name "op -->"}, _) $ p $ q) =
   37.19              Buildin("=>", [fm (not pos) p, fm pos q])
   37.20 -      | fm pos (Const(@{const_name "Not"}, _) $ p) =
   37.21 +      | fm pos (Const(@{const_name Not}, _) $ p) =
   37.22              Buildin("NOT", [fm (not pos) p])
   37.23 -      | fm pos (Const(@{const_name "True"}, _)) = TrueExpr
   37.24 -      | fm pos (Const(@{const_name "False"}, _)) = FalseExpr
   37.25 +      | fm pos (Const(@{const_name True}, _)) = TrueExpr
   37.26 +      | fm pos (Const(@{const_name False}, _)) = FalseExpr
   37.27        | fm pos (Const("SVC_Oracle.iff_keep", _) $ p $ q) =
   37.28               (*polarity doesn't matter*)
   37.29              Buildin("=", [fm pos p, fm pos q])
   37.30 @@ -225,7 +225,7 @@
   37.31              else fail t
   37.32        | fm pos t = var(t,[]);
   37.33        (*entry point, and translation of a meta-formula*)
   37.34 -      fun mt pos ((c as Const(@{const_name "Trueprop"}, _)) $ p) = fm pos (iff_tag p)
   37.35 +      fun mt pos ((c as Const(@{const_name Trueprop}, _)) $ p) = fm pos (iff_tag p)
   37.36          | mt pos ((c as Const("==>", _)) $ p $ q) =
   37.37              Buildin("=>", [mt (not pos) p, mt pos q])
   37.38          | mt pos t = fm pos (iff_tag t)  (*it might be a formula*)