# HG changeset patch
# User haftmann
# Date 1282226939 -7200
# Node ID 32ad17fe2b9c0bb86faf11fd644b5d33b6fb5f4e
# Parent  9926c47ad1a1c282db731f38b9a28bc286b9be2f
tuned quotes

diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Aug 19 16:08:59 2010 +0200
@@ -3301,10 +3301,10 @@
 ML {*
   fun reorder_bounds_tac prems i =
     let
-      fun variable_of_bound (Const (@{const_name "Trueprop"}, _) $
+      fun variable_of_bound (Const (@{const_name Trueprop}, _) $
                              (Const (@{const_name Set.member}, _) $
                               Free (name, _) $ _)) = name
-        | variable_of_bound (Const (@{const_name "Trueprop"}, _) $
+        | variable_of_bound (Const (@{const_name Trueprop}, _) $
                              (Const (@{const_name "op ="}, _) $
                               Free (name, _) $ _)) = name
         | variable_of_bound t = raise TERM ("variable_of_bound", [t])
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy	Thu Aug 19 16:08:59 2010 +0200
@@ -1960,12 +1960,12 @@
       @{code Imp} (fm_of_term ps vs t1, fm_of_term ps vs t2)
   | fm_of_term ps vs (@{term "Not"} $ t') =
       @{code NOT} (fm_of_term ps vs t')
-  | fm_of_term ps vs (Const (@{const_name "Ex"}, _) $ Abs (xn, xT, p)) =
+  | fm_of_term ps vs (Const (@{const_name Ex}, _) $ Abs (xn, xT, p)) =
       let
         val (xn', p') = variant_abs (xn, xT, p);
         val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
       in @{code E} (fm_of_term ps vs' p) end
-  | fm_of_term ps vs (Const (@{const_name "All"}, _) $ Abs (xn, xT, p)) =
+  | fm_of_term ps vs (Const (@{const_name All}, _) $ Abs (xn, xT, p)) =
       let
         val (xn', p') = variant_abs (xn, xT, p);
         val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Thu Aug 19 16:08:59 2010 +0200
@@ -2000,9 +2000,9 @@
   | fm_of_term vs (@{term "op |"} $ t1 $ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
   | fm_of_term vs (@{term "op -->"} $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
   | fm_of_term vs (@{term "Not"} $ t') = @{code NOT} (fm_of_term vs t')
-  | fm_of_term vs (Const (@{const_name "Ex"}, _) $ Abs (xn, xT, p)) =
+  | fm_of_term vs (Const (@{const_name Ex}, _) $ Abs (xn, xT, p)) =
       @{code E} (fm_of_term (("", dummyT) :: vs) p)
-  | fm_of_term vs (Const (@{const_name "All"}, _) $ Abs (xn, xT, p)) =
+  | fm_of_term vs (Const (@{const_name All}, _) $ Abs (xn, xT, p)) =
       @{code A} (fm_of_term (("", dummyT) ::  vs) p)
   | fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t);
 
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Thu Aug 19 16:08:59 2010 +0200
@@ -5845,9 +5845,9 @@
       @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
   | fm_of_term vs (@{term "Not"} $ t') =
       @{code NOT} (fm_of_term vs t')
-  | fm_of_term vs (Const (@{const_name "Ex"}, _) $ Abs (xn, xT, p)) =
+  | fm_of_term vs (Const (@{const_name Ex}, _) $ Abs (xn, xT, p)) =
       @{code E} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p)
-  | fm_of_term vs (Const (@{const_name "All"}, _) $ Abs (xn, xT, p)) =
+  | fm_of_term vs (Const (@{const_name All}, _) $ Abs (xn, xT, p)) =
       @{code A} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p)
   | fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t);
 
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Aug 19 16:08:59 2010 +0200
@@ -3015,9 +3015,9 @@
 
 fun fm_of_term m m' fm = 
  case fm of
-    Const(@{const_name "True"},_) => @{code T}
-  | Const(@{const_name "False"},_) => @{code F}
-  | Const(@{const_name "Not"},_)$p => @{code NOT} (fm_of_term m m' p)
+    Const(@{const_name True},_) => @{code T}
+  | Const(@{const_name False},_) => @{code F}
+  | Const(@{const_name Not},_)$p => @{code NOT} (fm_of_term m m' p)
   | Const(@{const_name "op &"},_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
   | Const(@{const_name "op |"},_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
   | Const(@{const_name "op -->"},_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
@@ -3028,13 +3028,13 @@
         @{code Lt} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
   | Const(@{const_name Orderings.less_eq},_)$p$q => 
         @{code Le} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
-  | Const(@{const_name "Ex"},_)$Abs(xn,xT,p) => 
+  | Const(@{const_name Ex},_)$Abs(xn,xT,p) => 
      let val (xn', p') =  variant_abs (xn,xT,p)
          val x = Free(xn',xT)
          fun incr i = i + 1
          val m0 = (x,0):: (map (apsnd incr) m)
       in @{code E} (fm_of_term m0 m' p') end
-  | Const(@{const_name "All"},_)$Abs(xn,xT,p) => 
+  | Const(@{const_name All},_)$Abs(xn,xT,p) => 
      let val (xn', p') =  variant_abs (xn,xT,p)
          val x = Free(xn',xT)
          fun incr i = i + 1
@@ -3045,8 +3045,8 @@
 
 fun term_of_fm T m m' t = 
   case t of
-    @{code T} => Const(@{const_name "True"},bT)
-  | @{code F} => Const(@{const_name "False"},bT)
+    @{code T} => Const(@{const_name True},bT)
+  | @{code F} => Const(@{const_name False},bT)
   | @{code NOT} p => nott $ (term_of_fm T m m' p)
   | @{code And} (p,q) => conjt $ (term_of_fm T m m' p) $ (term_of_fm T m m' q)
   | @{code Or} (p,q) => disjt $ (term_of_fm T m m' p) $ (term_of_fm T m m' q)
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Decision_Procs/cooper_tac.ML
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Thu Aug 19 16:08:59 2010 +0200
@@ -110,7 +110,7 @@
     fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
     (* The result of the quantifier elimination *)
     val (th, tac) = case (prop_of pre_thm) of
-        Const ("==>", _) $ (Const (@{const_name "Trueprop"}, _) $ t1) $ _ =>
+        Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
     let val pth = linzqe_oracle (cterm_of thy (Pattern.eta_long [] t1))
     in
           ((pth RS iffD2) RS pre_thm,
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Decision_Procs/ferrack_tac.ML
--- a/src/HOL/Decision_Procs/ferrack_tac.ML	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Thu Aug 19 16:08:59 2010 +0200
@@ -91,7 +91,7 @@
     fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
     (* The result of the quantifier elimination *)
     val (th, tac) = case prop_of pre_thm of
-        Const ("==>", _) $ (Const (@{const_name "Trueprop"}, _) $ t1) $ _ =>
+        Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
     let val pth = linr_oracle (ctxt, Pattern.eta_long [] t1)
     in 
           (trace_msg ("calling procedure with term:\n" ^
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Decision_Procs/ferrante_rackoff.ML
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Aug 19 16:08:59 2010 +0200
@@ -77,7 +77,7 @@
  fun main vs p =
   let
    val ((xn,ce),(x,fm)) = (case term_of p of
-                   Const(@{const_name "Ex"},_)$Abs(xn,xT,_) =>
+                   Const(@{const_name Ex},_)$Abs(xn,xT,_) =>
                         Thm.dest_comb p ||> Thm.dest_abs (SOME xn) |>> pair xn
                  | _ => raise CTERM ("main QE only treats existential quantifiers!", [p]))
    val cT = ctyp_of_term x
@@ -178,16 +178,16 @@
      Const (@{const_name "op ="}, T) $ _ $ _ =>
        if domain_type T = HOLogic.boolT then find_args bounds tm
        else Thm.dest_fun2 tm
-   | Const (@{const_name "Not"}, _) $ _ => h bounds (Thm.dest_arg tm)
-   | Const (@{const_name "All"}, _) $ _ => find_body bounds (Thm.dest_arg tm)
-   | Const (@{const_name "Ex"}, _) $ _ => find_body bounds (Thm.dest_arg tm)
+   | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
+   | Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
+   | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
    | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
    | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
    | Const ("==>", _) $ _ $ _ => find_args bounds tm
    | Const ("==", _) $ _ $ _ => find_args bounds tm
    | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
-   | Const (@{const_name "Trueprop"}, _) $ _ => h bounds (Thm.dest_arg tm)
+   | Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm)
    | _ => Thm.dest_fun2 tm)
   and find_args bounds tm =
            (h bounds (Thm.dest_arg tm) handle CTERM _ => Thm.dest_arg1 tm)
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Decision_Procs/langford.ML
--- a/src/HOL/Decision_Procs/langford.ML	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Decision_Procs/langford.ML	Thu Aug 19 16:08:59 2010 +0200
@@ -30,7 +30,7 @@
 
 fun basic_dloqe ctxt stupid dlo_qeth dlo_qeth_nolb dlo_qeth_noub gather ep = 
  case term_of ep of 
-  Const(@{const_name "Ex"},_)$_ => 
+  Const(@{const_name Ex},_)$_ => 
    let 
      val p = Thm.dest_arg ep
      val ths = simplify (HOL_basic_ss addsimps gather) (instantiate' [] [SOME p] stupid)
@@ -122,7 +122,7 @@
 local 
 fun proc ct = 
  case term_of ct of
-  Const(@{const_name "Ex"},_)$Abs (xn,_,_) => 
+  Const(@{const_name Ex},_)$Abs (xn,_,_) => 
    let 
     val e = Thm.dest_fun ct
     val (x,p) = Thm.dest_abs (SOME xn) (Thm.dest_arg ct)
@@ -179,16 +179,16 @@
      Const (@{const_name "op ="}, T) $ _ $ _ =>
        if domain_type T = HOLogic.boolT then find_args bounds tm
        else Thm.dest_fun2 tm
-   | Const (@{const_name "Not"}, _) $ _ => h bounds (Thm.dest_arg tm)
-   | Const (@{const_name "All"}, _) $ _ => find_body bounds (Thm.dest_arg tm)
+   | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
+   | Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
-   | Const (@{const_name "Ex"}, _) $ _ => find_body bounds (Thm.dest_arg tm)
+   | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
    | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
    | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
    | Const ("==>", _) $ _ $ _ => find_args bounds tm
    | Const ("==", _) $ _ $ _ => find_args bounds tm
-   | Const (@{const_name "Trueprop"}, _) $ _ => h bounds (Thm.dest_arg tm)
+   | Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm)
    | _ => Thm.dest_fun2 tm)
   and find_args bounds tm =
     (h bounds (Thm.dest_arg tm) handle CTERM _ => h bounds (Thm.dest_arg1 tm))
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Decision_Procs/mir_tac.ML
--- a/src/HOL/Decision_Procs/mir_tac.ML	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML	Thu Aug 19 16:08:59 2010 +0200
@@ -132,7 +132,7 @@
     fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
     (* The result of the quantifier elimination *)
     val (th, tac) = case (prop_of pre_thm) of
-        Const ("==>", _) $ (Const (@{const_name "Trueprop"}, _) $ t1) $ _ =>
+        Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
     let val pth =
           (* If quick_and_dirty then run without proof generation as oracle*)
              if !quick_and_dirty
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Import/shuffler.ML	Thu Aug 19 16:08:59 2010 +0200
@@ -60,14 +60,14 @@
 
 fun mk_meta_eq th =
     (case concl_of th of
-         Const(@{const_name "Trueprop"},_) $ (Const(@{const_name "op ="},_) $ _ $ _) => th RS eq_reflection
+         Const(@{const_name Trueprop},_) $ (Const(@{const_name "op ="},_) $ _ $ _) => th RS eq_reflection
        | Const("==",_) $ _ $ _ => th
        | _ => raise THM("Not an equality",0,[th]))
     handle _ => raise THM("Couldn't make meta equality",0,[th])  (* FIXME avoid handle _ *)
 
 fun mk_obj_eq th =
     (case concl_of th of
-         Const(@{const_name "Trueprop"},_) $ (Const(@{const_name "op ="},_) $ _ $ _) => th
+         Const(@{const_name Trueprop},_) $ (Const(@{const_name "op ="},_) $ _ $ _) => th
        | Const("==",_) $ _ $ _ => th RS meta_eq_to_obj_eq
        | _ => raise THM("Not an equality",0,[th]))
     handle _ => raise THM("Couldn't make object equality",0,[th])  (* FIXME avoid handle _ *)
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Library/Eval_Witness.thy
--- a/src/HOL/Library/Eval_Witness.thy	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Library/Eval_Witness.thy	Thu Aug 19 16:08:59 2010 +0200
@@ -63,7 +63,7 @@
     else error ("Type " ^ quote (Syntax.string_of_typ_global thy T) ^ " not allowed for ML witnesses")
 
   fun dest_exs  0 t = t
-    | dest_exs n (Const (@{const_name "Ex"}, _) $ Abs (v,T,b)) = 
+    | dest_exs n (Const (@{const_name Ex}, _) $ Abs (v,T,b)) = 
       Abs (v, check_type T, dest_exs (n - 1) b)
     | dest_exs _ _ = sys_error "dest_exs";
   val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Library/positivstellensatz.ML
--- a/src/HOL/Library/positivstellensatz.ML	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Library/positivstellensatz.ML	Thu Aug 19 16:08:59 2010 +0200
@@ -498,7 +498,7 @@
  val strip_exists =
   let fun h (acc, t) =
    case (term_of t) of
-    Const(@{const_name "Ex"},_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
+    Const(@{const_name Ex},_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
   | _ => (acc,t)
   in fn t => h ([],t)
   end
@@ -515,7 +515,7 @@
  fun mk_ex v t = Thm.capply (ext (ctyp_of_term v)) (Thm.cabs v t)
 
  fun choose v th th' = case concl_of th of 
-   @{term Trueprop} $ (Const(@{const_name "Ex"},_)$_) => 
+   @{term Trueprop} $ (Const(@{const_name Ex},_)$_) => 
     let
      val p = (funpow 2 Thm.dest_arg o cprop_of) th
      val T = (hd o Thm.dest_ctyp o ctyp_of_term) p
@@ -533,7 +533,7 @@
  val strip_forall =
   let fun h (acc, t) =
    case (term_of t) of
-    Const(@{const_name "All"},_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
+    Const(@{const_name All},_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
   | _ => (acc,t)
   in fn t => h ([],t)
   end
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Thu Aug 19 16:08:59 2010 +0200
@@ -183,7 +183,7 @@
   end;
 
 fun mk_not_sym ths = maps (fn th => case prop_of th of
-    _ $ (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _)) => [th, th RS not_sym]
+    _ $ (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _)) => [th, th RS not_sym]
   | _ => [th]) ths;
 
 fun fresh_const T U = Const ("Nominal.fresh", T --> U --> HOLogic.boolT);
@@ -1372,7 +1372,7 @@
                             SUBGOAL (fn (t, i) => case Logic.strip_assums_concl t of
                                 _ $ (Const ("Nominal.fresh", _) $ _ $ _) =>
                                   simp_tac ind_ss1' i
-                              | _ $ (Const (@{const_name "Not"}, _) $ _) =>
+                              | _ $ (Const (@{const_name Not}, _) $ _) =>
                                   resolve_tac freshs2' i
                               | _ => asm_simp_tac (HOL_basic_ss addsimps
                                   pt2_atoms addsimprocs [perm_simproc]) i)) 1])
@@ -1671,7 +1671,7 @@
     val rec_unique_frees' =
       Datatype_Prop.indexify_names (replicate (length recTs) "y") ~~ rec_result_Ts;
     val rec_unique_concls = map (fn ((x, U), R) =>
-        Const (@{const_name "Ex1"}, (U --> HOLogic.boolT) --> HOLogic.boolT) $
+        Const (@{const_name Ex1}, (U --> HOLogic.boolT) --> HOLogic.boolT) $
           Abs ("y", U, R $ Free x $ Bound 0))
       (rec_unique_frees ~~ rec_result_Ts ~~ rec_sets);
 
@@ -1777,7 +1777,7 @@
                       | _ => false) prems';
                     val fresh_prems = filter (fn th => case prop_of th of
                         _ $ (Const ("Nominal.fresh", _) $ _ $ _) => true
-                      | _ $ (Const (@{const_name "Not"}, _) $ _) => true
+                      | _ $ (Const (@{const_name Not}, _) $ _) => true
                       | _ => false) prems';
                     val Ts = map fastype_of boundsl;
 
@@ -1879,7 +1879,7 @@
                       end) rec_prems2;
 
                     val ihs = filter (fn th => case prop_of th of
-                      _ $ (Const (@{const_name "All"}, _) $ _) => true | _ => false) prems';
+                      _ $ (Const (@{const_name All}, _) $ _) => true | _ => false) prems';
 
                     (** pi1 o rs = pi2 o vs , rs = pi1^-1 o pi2 o vs **)
                     val _ = warning "step 7: pi1 o rs = pi2 o vs , rs = pi1^-1 o pi2 o vs";
@@ -2022,7 +2022,7 @@
           (reccomb_names ~~ recTs ~~ rec_result_Ts))
       |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
           (Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
-           Const (@{const_name "The"}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
+           Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
              set $ Free ("x", T) $ Free ("y", T'))))))
                (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts));
 
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Aug 19 16:08:59 2010 +0200
@@ -78,7 +78,7 @@
   | split_conj _ _ _ _ = NONE;
 
 fun strip_all [] t = t
-  | strip_all (_ :: xs) (Const (@{const_name "All"}, _) $ Abs (s, T, t)) = strip_all xs t;
+  | strip_all (_ :: xs) (Const (@{const_name All}, _) $ Abs (s, T, t)) = strip_all xs t;
 
 (*********************************************************************)
 (* maps  R ... & (ALL pi_1 ... pi_n z. P z (pi_1 o ... o pi_n o t))  *)
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Thu Aug 19 16:08:59 2010 +0200
@@ -82,7 +82,7 @@
   | split_conj _ _ _ _ = NONE;
 
 fun strip_all [] t = t
-  | strip_all (_ :: xs) (Const (@{const_name "All"}, _) $ Abs (s, T, t)) = strip_all xs t;
+  | strip_all (_ :: xs) (Const (@{const_name All}, _) $ Abs (s, T, t)) = strip_all xs t;
 
 (*********************************************************************)
 (* maps  R ... & (ALL pi_1 ... pi_n z. P z (pi_1 o ... o pi_n o t))  *)
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Nominal/nominal_thmdecls.ML
--- a/src/HOL/Nominal/nominal_thmdecls.ML	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML	Thu Aug 19 16:08:59 2010 +0200
@@ -135,7 +135,7 @@
     val thy = Context.theory_of context
     val thms_to_be_added = (case (prop_of orig_thm) of
         (* case: eqvt-lemma is of the implicational form *)
-        (Const("==>", _) $ (Const (@{const_name "Trueprop"},_) $ hyp) $ (Const (@{const_name "Trueprop"},_) $ concl)) =>
+        (Const("==>", _) $ (Const (@{const_name Trueprop},_) $ hyp) $ (Const (@{const_name Trueprop},_) $ concl)) =>
           let
             val (pi,typi) = get_pi concl thy
           in
@@ -147,7 +147,7 @@
              else raise EQVT_FORM "Type Implication"
           end
        (* case: eqvt-lemma is of the equational form *)
-      | (Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, _) $
+      | (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $
             (Const (@{const_name "perm"},typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
            (if (apply_pi lhs (pi,typi)) = rhs
                then [orig_thm]
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Statespace/distinct_tree_prover.ML
--- a/src/HOL/Statespace/distinct_tree_prover.ML	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Statespace/distinct_tree_prover.ML	Thu Aug 19 16:08:59 2010 +0200
@@ -343,7 +343,7 @@
   end handle Option => NONE)
 
 fun distinctTree_tac names ctxt 
-      (Const (@{const_name "Trueprop"},_) $ (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op ="}, _) $ x $ y)), i) =
+      (Const (@{const_name Trueprop},_) $ (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, _) $ x $ y)), i) =
   (case get_fst_success (neq_x_y ctxt x y) names of
      SOME neq => rtac neq i
    | NONE => no_tac)
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Statespace/state_fun.ML	Thu Aug 19 16:08:59 2010 +0200
@@ -43,9 +43,9 @@
 val conj_True = thm "conj_True";
 val conj_cong = thm "conj_cong";
 
-fun isFalse (Const (@{const_name "False"},_)) = true
+fun isFalse (Const (@{const_name False},_)) = true
   | isFalse _ = false;
-fun isTrue (Const (@{const_name "True"},_)) = true
+fun isTrue (Const (@{const_name True},_)) = true
   | isTrue _ = false;
 
 in
@@ -305,10 +305,10 @@
 
        in
          (case t of
-           (Const (@{const_name "Ex"},Tex)$Abs(s,T,t)) =>
+           (Const (@{const_name Ex},Tex)$Abs(s,T,t)) =>
              (let val (eq,eT,nT,swap) = mkeq (dest_sel_eq t) 0;
                   val prop = list_all ([("n",nT),("x",eT)],
-                              Logic.mk_equals (Const (@{const_name "Ex"},Tex)$Abs(s,T,eq),
+                              Logic.mk_equals (Const (@{const_name Ex},Tex)$Abs(s,T,eq),
                                                HOLogic.true_const));
                   val thm = Drule.export_without_context (prove prop);
                   val thm' = if swap then swap_ex_eq OF [thm] else thm
@@ -367,7 +367,7 @@
      val (lookup_ss,ex_lookup_ss,simprocs_active) = StateFunData.get ctxt;
      val (lookup_ss', ex_lookup_ss') = 
            (case (concl_of thm) of
-            (_$((Const (@{const_name "Ex"},_)$_))) => (lookup_ss, ex_lookup_ss addsimps [thm])
+            (_$((Const (@{const_name Ex},_)$_))) => (lookup_ss, ex_lookup_ss addsimps [thm])
             | _ => (lookup_ss addsimps [thm], ex_lookup_ss))
      fun activate_simprocs ctxt =
           if simprocs_active then ctxt
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML	Thu Aug 19 16:08:59 2010 +0200
@@ -222,8 +222,8 @@
   end handle Option => NONE)
 
 fun distinctTree_tac ctxt
-      (Const (@{const_name "Trueprop"},_) $
-        (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op ="}, _) $ (x as Free _)$ (y as Free _))), i) =
+      (Const (@{const_name Trueprop},_) $
+        (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, _) $ (x as Free _)$ (y as Free _))), i) =
   (case (neq_x_y ctxt x y) of
      SOME neq => rtac neq i
    | NONE => no_tac)
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Thu Aug 19 16:08:59 2010 +0200
@@ -392,7 +392,7 @@
     (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
     val ihyp = Term.all domT $ Abs ("z", domT,
       Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
-        HOLogic.mk_Trueprop (Const (@{const_name "Ex1"}, (ranT --> boolT) --> boolT) $
+        HOLogic.mk_Trueprop (Const (@{const_name Ex1}, (ranT --> boolT) --> boolT) $
           Abs ("y", ranT, G $ Bound 1 $ Bound 0))))
       |> cterm_of thy
 
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Aug 19 16:08:59 2010 +0200
@@ -147,7 +147,7 @@
 
 fun Trueprop_conv cv ct =
   case Thm.term_of ct of
-    Const (@{const_name "Trueprop"}, _) $ _ => Conv.arg_conv cv ct  
+    Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct  
   | _ => raise Fail "Trueprop_conv"
 
 fun preprocess_intro thy rule =
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Aug 19 16:08:59 2010 +0200
@@ -411,7 +411,7 @@
 fun conjuncts t = conjuncts_aux t [];
 
 fun is_equationlike_term (Const ("==", _) $ _ $ _) = true
-  | is_equationlike_term (Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _)) = true
+  | is_equationlike_term (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _)) = true
   | is_equationlike_term _ = false
   
 val is_equationlike = is_equationlike_term o prop_of 
@@ -479,7 +479,7 @@
 
 fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t)
 
-fun strip_ex (Const (@{const_name "Ex"}, _) $ Abs (x, T, t)) =
+fun strip_ex (Const (@{const_name Ex}, _) $ Abs (x, T, t)) =
   let
     val (xTs, t') = strip_ex t
   in
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Aug 19 16:08:59 2010 +0200
@@ -576,7 +576,7 @@
 
 fun Trueprop_conv cv ct =
   case Thm.term_of ct of
-    Const (@{const_name "Trueprop"}, _) $ _ => Conv.arg_conv cv ct  
+    Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct  
   | _ => raise Fail "Trueprop_conv"
 
 fun preprocess_intro thy rule =
@@ -587,7 +587,7 @@
 
 fun preprocess_elim ctxt elimrule =
   let
-    fun replace_eqs (Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, T) $ lhs $ rhs)) =
+    fun replace_eqs (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, T) $ lhs $ rhs)) =
        HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
      | replace_eqs t = t
     val thy = ProofContext.theory_of ctxt
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu Aug 19 16:08:59 2010 +0200
@@ -111,7 +111,7 @@
 
 fun mk_meta_equation th =
   case prop_of th of
-    Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _) => th RS @{thm eq_reflection}
+    Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _) => th RS @{thm eq_reflection}
   | _ => th
 
 val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp}
@@ -215,12 +215,12 @@
 val logic_operator_names =
   [@{const_name "=="}, 
    @{const_name "==>"},
-   @{const_name "Trueprop"},
-   @{const_name "Not"},
+   @{const_name Trueprop},
+   @{const_name Not},
    @{const_name "op ="},
    @{const_name "op -->"},
-   @{const_name "All"},
-   @{const_name "Ex"}, 
+   @{const_name All},
+   @{const_name Ex}, 
    @{const_name "op &"},
    @{const_name "op |"}]
 
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Thu Aug 19 16:08:59 2010 +0200
@@ -86,9 +86,9 @@
    map instantiate rew_ths
  end
 
-fun is_compound ((Const (@{const_name "Not"}, _)) $ t) =
+fun is_compound ((Const (@{const_name Not}, _)) $ t) =
     error "is_compound: Negation should not occur; preprocessing is defect"
-  | is_compound ((Const (@{const_name "Ex"}, _)) $ _) = true
+  | is_compound ((Const (@{const_name Ex}, _)) $ _) = true
   | is_compound ((Const (@{const_name "op |"}, _)) $ _ $ _) = true
   | is_compound ((Const (@{const_name "op &"}, _)) $ _ $ _) =
     error "is_compound: Conjunction should not occur; preprocessing is defect"
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Thu Aug 19 16:08:59 2010 +0200
@@ -622,9 +622,9 @@
       Proc.Iff (fm_of_term ps vs t1, fm_of_term ps vs t2)
   | fm_of_term ps vs (Const (@{const_name Not}, _) $ t') =
       Proc.Not (fm_of_term ps vs t')
-  | fm_of_term ps vs (Const (@{const_name "Ex"}, _) $ Abs abs) =
+  | fm_of_term ps vs (Const (@{const_name Ex}, _) $ Abs abs) =
       Proc.E (uncurry (fm_of_term ps) (descend vs abs))
-  | fm_of_term ps vs (Const (@{const_name "All"}, _) $ Abs abs) =
+  | fm_of_term ps vs (Const (@{const_name All}, _) $ Abs abs) =
       Proc.A (uncurry (fm_of_term ps) (descend vs abs))
   | fm_of_term ps vs (@{term "op = :: int => _"} $ t1 $ t2) =
       Proc.Eq (Proc.Sub (num_of_term vs t1, num_of_term vs t2))
@@ -694,7 +694,7 @@
 
 fun strip_objall ct = 
  case term_of ct of 
-  Const (@{const_name "All"}, _) $ Abs (xn,xT,p) => 
+  Const (@{const_name All}, _) $ Abs (xn,xT,p) => 
    let val (a,(v,t')) = (apsnd (Thm.dest_abs (SOME xn)) o Thm.dest_comb) ct
    in apfst (cons (a,v)) (strip_objall t')
    end
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Tools/Quotient/quotient_term.ML
--- a/src/HOL/Tools/Quotient/quotient_term.ML	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Thu Aug 19 16:08:59 2010 +0200
@@ -490,16 +490,16 @@
          else mk_bex1_rel $ resrel $ subtrm
        end
 
-  | (Const (@{const_name "Ex1"}, ty) $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
+  | (Const (@{const_name Ex1}, ty) $ t, Const (@{const_name Ex1}, ty') $ t') =>
        let
          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
        in
-         if ty = ty' then Const (@{const_name "Ex1"}, ty) $ subtrm
+         if ty = ty' then Const (@{const_name Ex1}, ty) $ subtrm
          else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
        end
 
   | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
-     Const (@{const_name "All"}, ty') $ t') =>
+     Const (@{const_name All}, ty') $ t') =>
        let
          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
          val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
@@ -510,7 +510,7 @@
        end
 
   | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
-     Const (@{const_name "Ex"}, ty') $ t') =>
+     Const (@{const_name Ex}, ty') $ t') =>
        let
          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
          val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
@@ -520,7 +520,7 @@
          else mk_bex $ (mk_resp $ resrel) $ subtrm
        end
 
-  | (Const (@{const_name "Bex1_rel"}, ty) $ resrel $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
+  | (Const (@{const_name "Bex1_rel"}, ty) $ resrel $ t, Const (@{const_name Ex1}, ty') $ t') =>
        let
          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
          val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
@@ -638,10 +638,10 @@
    as the type of subterms needs to be calculated   *)
 fun inj_repabs_trm ctxt (rtrm, qtrm) =
  case (rtrm, qtrm) of
-    (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
+    (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name All}, _) $ t') =>
        Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
 
-  | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
+  | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name Ex}, _) $ t') =>
        Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
 
   | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) =>
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/choice_specification.ML	Thu Aug 19 16:08:59 2010 +0200
@@ -24,7 +24,7 @@
     fun mk_definitional [] arg = arg
       | mk_definitional ((thname,cname,covld)::cos) (thy,thm) =
         case HOLogic.dest_Trueprop (concl_of thm) of
-            Const(@{const_name "Ex"},_) $ P =>
+            Const(@{const_name Ex},_) $ P =>
             let
                 val ctype = domain_type (type_of P)
                 val cname_full = Sign.intern_const thy cname
@@ -51,7 +51,7 @@
                 end
               | process ((thname,cname,covld)::cos) (thy,tm) =
                 case tm of
-                    Const(@{const_name "Ex"},_) $ P =>
+                    Const(@{const_name Ex},_) $ P =>
                     let
                         val ctype = domain_type (type_of P)
                         val cname_full = Sign.intern_const thy cname
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Tools/cnf_funcs.ML
--- a/src/HOL/Tools/cnf_funcs.ML	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML	Thu Aug 19 16:08:59 2010 +0200
@@ -93,16 +93,16 @@
 
 val cnftac_eq_imp        = @{lemma "[| P = Q; P |] ==> Q" by auto};
 
-fun is_atom (Const (@{const_name "False"}, _))                                           = false
-  | is_atom (Const (@{const_name "True"}, _))                                            = false
+fun is_atom (Const (@{const_name False}, _))                                           = false
+  | is_atom (Const (@{const_name True}, _))                                            = false
   | is_atom (Const (@{const_name "op &"}, _) $ _ $ _)                                    = false
   | is_atom (Const (@{const_name "op |"}, _) $ _ $ _)                                    = false
   | is_atom (Const (@{const_name "op -->"}, _) $ _ $ _)                                  = false
   | is_atom (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ _ $ _)       = false
-  | is_atom (Const (@{const_name "Not"}, _) $ _)                                         = false
+  | is_atom (Const (@{const_name Not}, _) $ _)                                         = false
   | is_atom _                                                              = true;
 
-fun is_literal (Const (@{const_name "Not"}, _) $ x) = is_atom x
+fun is_literal (Const (@{const_name Not}, _) $ x) = is_atom x
   | is_literal x                      = is_atom x;
 
 fun is_clause (Const (@{const_name "op |"}, _) $ x $ y) = is_clause x andalso is_clause y
@@ -118,7 +118,7 @@
 fun clause_is_trivial c =
 	let
 		(* Term.term -> Term.term *)
-		fun dual (Const (@{const_name "Not"}, _) $ x) = x
+		fun dual (Const (@{const_name Not}, _) $ x) = x
 		  | dual x                      = HOLogic.Not $ x
 		(* Term.term list -> bool *)
 		fun has_duals []      = false
@@ -214,32 +214,32 @@
 	in
 		make_nnf_iff OF [thm1, thm2, thm3, thm4]
 	end
-  | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ Const (@{const_name "False"}, _)) =
+  | make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name False}, _)) =
 	make_nnf_not_false
-  | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ Const (@{const_name "True"}, _)) =
+  | make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name True}, _)) =
 	make_nnf_not_true
-  | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op &"}, _) $ x $ y)) =
+  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op &"}, _) $ x $ y)) =
 	let
 		val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
 		val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
 	in
 		make_nnf_not_conj OF [thm1, thm2]
 	end
-  | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op |"}, _) $ x $ y)) =
+  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op |"}, _) $ x $ y)) =
 	let
 		val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
 		val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
 	in
 		make_nnf_not_disj OF [thm1, thm2]
 	end
-  | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op -->"}, _) $ x $ y)) =
+  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op -->"}, _) $ x $ y)) =
 	let
 		val thm1 = make_nnf_thm thy x
 		val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
 	in
 		make_nnf_not_imp OF [thm1, thm2]
 	end
-  | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ x $ y)) =
+  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ x $ y)) =
 	let
 		val thm1 = make_nnf_thm thy x
 		val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
@@ -248,7 +248,7 @@
 	in
 		make_nnf_not_iff OF [thm1, thm2, thm3, thm4]
 	end
-  | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "Not"}, _) $ x)) =
+  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name Not}, _) $ x)) =
 	let
 		val thm1 = make_nnf_thm thy x
 	in
@@ -430,7 +430,7 @@
 				in
 					make_cnf_disj_conj_r OF [thm1, thm2]  (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
 				end
-			  | make_cnfx_disj_thm (Const (@{const_name "Ex"}, _) $ x') y' =
+			  | make_cnfx_disj_thm (Const (@{const_name Ex}, _) $ x') y' =
 				let
 					val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_l   (* ((Ex x') | y') = (Ex (x' | y')) *)
 					val var  = new_free ()
@@ -441,7 +441,7 @@
 				in
 					iff_trans OF [thm1, thm5]  (* ((Ex x') | y') = (Ex v. body') *)
 				end
-			  | make_cnfx_disj_thm x' (Const (@{const_name "Ex"}, _) $ y') =
+			  | make_cnfx_disj_thm x' (Const (@{const_name Ex}, _) $ y') =
 				let
 					val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_r   (* (x' | (Ex y')) = (Ex (x' | y')) *)
 					val var  = new_free ()
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/groebner.ML	Thu Aug 19 16:08:59 2010 +0200
@@ -405,7 +405,7 @@
 val mk_comb = capply;
 fun is_neg t =
     case term_of t of
-      (Const(@{const_name "Not"},_)$p) => true
+      (Const(@{const_name Not},_)$p) => true
     | _  => false;
 fun is_eq t =
  case term_of t of
@@ -430,14 +430,14 @@
 val strip_exists =
  let fun h (acc, t) =
       case (term_of t) of
-       Const(@{const_name "Ex"},_)$Abs(x,T,p) => h (dest_abs NONE (dest_arg t) |>> (fn v => v::acc))
+       Const(@{const_name Ex},_)$Abs(x,T,p) => h (dest_abs NONE (dest_arg t) |>> (fn v => v::acc))
      | _ => (acc,t)
  in fn t => h ([],t)
  end;
 
 fun is_forall t =
  case term_of t of
-  (Const(@{const_name "All"},_)$Abs(_,_,_)) => true
+  (Const(@{const_name All},_)$Abs(_,_,_)) => true
 | _ => false;
 
 val mk_object_eq = fn th => th COMP meta_eq_to_obj_eq;
@@ -522,7 +522,7 @@
  fun mk_ex v t = Thm.capply (ext (ctyp_of_term v)) (Thm.cabs v t)
 
 fun choose v th th' = case concl_of th of 
-  @{term Trueprop} $ (Const(@{const_name "Ex"},_)$_) => 
+  @{term Trueprop} $ (Const(@{const_name Ex},_)$_) => 
    let
     val p = (funpow 2 Thm.dest_arg o cprop_of) th
     val T = (hd o Thm.dest_ctyp o ctyp_of_term) p
@@ -926,9 +926,9 @@
     Const (@{const_name "op ="}, T) $ _ $ _ =>
       if domain_type T = HOLogic.boolT then find_args bounds tm
       else dest_arg tm
-  | Const (@{const_name "Not"}, _) $ _ => find_term bounds (dest_arg tm)
-  | Const (@{const_name "All"}, _) $ _ => find_body bounds (dest_arg tm)
-  | Const (@{const_name "Ex"}, _) $ _ => find_body bounds (dest_arg tm)
+  | Const (@{const_name Not}, _) $ _ => find_term bounds (dest_arg tm)
+  | Const (@{const_name All}, _) $ _ => find_body bounds (dest_arg tm)
+  | Const (@{const_name Ex}, _) $ _ => find_body bounds (dest_arg tm)
   | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
   | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
   | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Thu Aug 19 16:08:59 2010 +0200
@@ -46,12 +46,12 @@
 val mk_Trueprop = HOLogic.mk_Trueprop;
 
 fun atomize thm = case Thm.prop_of thm of
-    Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op &"}, _) $ _ $ _) =>
+    Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op &"}, _) $ _ $ _) =>
     atomize (thm RS conjunct1) @ atomize (thm RS conjunct2)
   | _ => [thm];
 
-fun neg_prop ((TP as Const(@{const_name "Trueprop"}, _)) $ (Const (@{const_name Not}, _) $ t)) = TP $ t
-  | neg_prop ((TP as Const(@{const_name "Trueprop"}, _)) $ t) = TP $ (HOLogic.Not $t)
+fun neg_prop ((TP as Const(@{const_name Trueprop}, _)) $ (Const (@{const_name Not}, _) $ t)) = TP $ t
+  | neg_prop ((TP as Const(@{const_name Trueprop}, _)) $ t) = TP $ (HOLogic.Not $t)
   | neg_prop t = raise TERM ("neg_prop", [t]);
 
 fun is_False thm =
@@ -258,10 +258,10 @@
   | negate NONE                        = NONE;
 
 fun decomp_negation data
-  ((Const (@{const_name "Trueprop"}, _)) $ (Const (rel, T) $ lhs $ rhs)) : decomp option =
+  ((Const (@{const_name Trueprop}, _)) $ (Const (rel, T) $ lhs $ rhs)) : decomp option =
       decomp_typecheck data (T, (rel, lhs, rhs))
-  | decomp_negation data ((Const (@{const_name "Trueprop"}, _)) $
-  (Const (@{const_name "Not"}, _) $ (Const (rel, T) $ lhs $ rhs))) =
+  | decomp_negation data ((Const (@{const_name Trueprop}, _)) $
+  (Const (@{const_name Not}, _) $ (Const (rel, T) $ lhs $ rhs))) =
       negate (decomp_typecheck data (T, (rel, lhs, rhs)))
   | decomp_negation data _ =
       NONE;
@@ -273,7 +273,7 @@
   in decomp_negation (thy, discrete, inj_consts) end;
 
 fun domain_is_nat (_ $ (Const (_, T) $ _ $ _))                      = nT T
-  | domain_is_nat (_ $ (Const (@{const_name "Not"}, _) $ (Const (_, T) $ _ $ _))) = nT T
+  | domain_is_nat (_ $ (Const (@{const_name Not}, _) $ (Const (_, T) $ _ $ _))) = nT T
   | domain_is_nat _                                                 = false;
 
 
@@ -659,7 +659,7 @@
 
 fun negated_term_occurs_positively (terms : term list) : bool =
   List.exists
-    (fn (Trueprop $ (Const (@{const_name "Not"}, _) $ t)) =>
+    (fn (Trueprop $ (Const (@{const_name Not}, _) $ t)) =>
       member Pattern.aeconv terms (Trueprop $ t)
       | _ => false)
     terms;
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Tools/prop_logic.ML
--- a/src/HOL/Tools/prop_logic.ML	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/prop_logic.ML	Thu Aug 19 16:08:59 2010 +0200
@@ -391,11 +391,11 @@
 				next_idx_is_valid := true;
 				Unsynchronized.inc next_idx
 			)
-		fun aux (Const (@{const_name "True"}, _))         table =
+		fun aux (Const (@{const_name True}, _))         table =
 			(True, table)
-		  | aux (Const (@{const_name "False"}, _))        table =
+		  | aux (Const (@{const_name False}, _))        table =
 			(False, table)
-		  | aux (Const (@{const_name "Not"}, _) $ x)      table =
+		  | aux (Const (@{const_name Not}, _) $ x)      table =
 			apfst Not (aux x table)
 		  | aux (Const (@{const_name "op |"}, _) $ x $ y) table =
 			let
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Tools/sat_funcs.ML
--- a/src/HOL/Tools/sat_funcs.ML	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/sat_funcs.ML	Thu Aug 19 16:08:59 2010 +0200
@@ -217,7 +217,7 @@
 	(* Thm.cterm -> int option *)
 	fun index_of_literal chyp = (
 		case (HOLogic.dest_Trueprop o Thm.term_of) chyp of
-		  (Const (@{const_name "Not"}, _) $ atom) =>
+		  (Const (@{const_name Not}, _) $ atom) =>
 			SOME (~ (the (Termtab.lookup atom_table atom)))
 		| atom =>
 			SOME (the (Termtab.lookup atom_table atom))
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Tools/simpdata.ML
--- a/src/HOL/Tools/simpdata.ML	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/simpdata.ML	Thu Aug 19 16:08:59 2010 +0200
@@ -45,7 +45,7 @@
   (*expects Trueprop if not == *)
   of Const (@{const_name "=="},_) $ _ $ _ => th
    | _ $ (Const (@{const_name "op ="}, _) $ _ $ _) => mk_meta_eq th
-   | _ $ (Const (@{const_name "Not"}, _) $ _) => th RS @{thm Eq_FalseI}
+   | _ $ (Const (@{const_name Not}, _) $ _) => th RS @{thm Eq_FalseI}
    | _ => th RS @{thm Eq_TrueI}
 
 fun mk_eq_True (_: simpset) r =
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/ex/SVC_Oracle.thy
--- a/src/HOL/ex/SVC_Oracle.thy	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy	Thu Aug 19 16:08:59 2010 +0200
@@ -91,15 +91,15 @@
     and fm ((c as Const(@{const_name "op &"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
       | fm ((c as Const(@{const_name "op |"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
       | fm ((c as Const(@{const_name "op -->"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
-      | fm ((c as Const(@{const_name "Not"}, _)) $ p) = c $ (fm p)
-      | fm ((c as Const(@{const_name "True"}, _))) = c
-      | fm ((c as Const(@{const_name "False"}, _))) = c
+      | fm ((c as Const(@{const_name Not}, _)) $ p) = c $ (fm p)
+      | fm ((c as Const(@{const_name True}, _))) = c
+      | fm ((c as Const(@{const_name False}, _))) = c
       | fm (t as Const(@{const_name "op ="},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
       | fm (t as Const(@{const_name Orderings.less},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
       | fm (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
       | fm t = replace t
     (*entry point, and abstraction of a meta-formula*)
-    fun mt ((c as Const(@{const_name "Trueprop"}, _)) $ p) = c $ (fm p)
+    fun mt ((c as Const(@{const_name Trueprop}, _)) $ p) = c $ (fm p)
       | mt ((c as Const("==>", _)) $ p $ q)  = c $ (mt p) $ (mt q)
       | mt t = fm t  (*it might be a formula*)
   in (list_all (params, mt body), !pairs) end;
diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/ex/svc_funcs.ML
--- a/src/HOL/ex/svc_funcs.ML	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/ex/svc_funcs.ML	Thu Aug 19 16:08:59 2010 +0200
@@ -92,9 +92,9 @@
              Const(@{const_name "op &"}, _)   => apply c (map tag ts)
            | Const(@{const_name "op |"}, _)   => apply c (map tag ts)
            | Const(@{const_name "op -->"}, _) => apply c (map tag ts)
-           | Const(@{const_name "Not"}, _)    => apply c (map tag ts)
-           | Const(@{const_name "True"}, _)   => (c, false)
-           | Const(@{const_name "False"}, _)  => (c, false)
+           | Const(@{const_name Not}, _)    => apply c (map tag ts)
+           | Const(@{const_name True}, _)   => (c, false)
+           | Const(@{const_name False}, _)  => (c, false)
            | Const(@{const_name "op ="}, Type ("fun", [T,_])) =>
                  if T = HOLogic.boolT then
                      (*biconditional: with int/nat comparisons below?*)
@@ -189,10 +189,10 @@
             Buildin("OR", [fm pos p, fm pos q])
       | fm pos (Const(@{const_name "op -->"}, _) $ p $ q) =
             Buildin("=>", [fm (not pos) p, fm pos q])
-      | fm pos (Const(@{const_name "Not"}, _) $ p) =
+      | fm pos (Const(@{const_name Not}, _) $ p) =
             Buildin("NOT", [fm (not pos) p])
-      | fm pos (Const(@{const_name "True"}, _)) = TrueExpr
-      | fm pos (Const(@{const_name "False"}, _)) = FalseExpr
+      | fm pos (Const(@{const_name True}, _)) = TrueExpr
+      | fm pos (Const(@{const_name False}, _)) = FalseExpr
       | fm pos (Const("SVC_Oracle.iff_keep", _) $ p $ q) =
              (*polarity doesn't matter*)
             Buildin("=", [fm pos p, fm pos q])
@@ -225,7 +225,7 @@
             else fail t
       | fm pos t = var(t,[]);
       (*entry point, and translation of a meta-formula*)
-      fun mt pos ((c as Const(@{const_name "Trueprop"}, _)) $ p) = fm pos (iff_tag p)
+      fun mt pos ((c as Const(@{const_name Trueprop}, _)) $ p) = fm pos (iff_tag p)
         | mt pos ((c as Const("==>", _)) $ p $ q) =
             Buildin("=>", [mt (not pos) p, mt pos q])
         | mt pos t = fm pos (iff_tag t)  (*it might be a formula*)