# HG changeset patch
# User haftmann
# Date 1179424180 -7200
# Node ID d4f3b015b50b02f9a87d37cc25bac87b5f0046dd
# Parent  5f82c5f8478e94c0b5036eed89b21ef74cf7e858
canonical prefixing of class constants

diff -r 5f82c5f8478e -r d4f3b015b50b NEWS
--- a/NEWS	Thu May 17 19:49:21 2007 +0200
+++ b/NEWS	Thu May 17 19:49:40 2007 +0200
@@ -530,6 +530,15 @@
 
 *** HOL ***
 
+* Constant renames due to introduction of canonical name prefixing for
+  class package:
+
+    HOL.abs ~> HOL.minus_class.abs
+    HOL.divide ~> HOL.divide_class.divide
+    Nat.power ~> Nat.power_class.power
+    Nat.size ~> Nat.size_class.size
+    Numeral.number_of ~> Numeral.number_class.number_of
+
 * case expressions and primrec: missing cases now mapped to "undefined"
 instead of "arbitrary"
 
@@ -675,7 +684,7 @@
 type "'a::size ==> bool"
 
 * Renamed constants "Divides.op div", "Divides.op mod" and "Divides.op
-dvd" to "Divides.div", "Divides.mod" and "Divides.dvd". INCOMPATIBILITY.
+dvd" to "Divides.div_class.div", "Divides.div_class.mod" and "Divides.dvd". INCOMPATIBILITY.
 
 * Added method "lexicographic_order" automatically synthesizes
 termination relations as lexicographic combinations of size measures
@@ -708,7 +717,7 @@
 rarely occuring name references (e.g. ``List.op mem.simps'') require
 renaming (e.g. ``List.memberl.simps'').
 
-* Renamed constants "0" to "HOL.zero" and "1" to "HOL.one".
+* Renamed constants "0" to "HOL.zero_class.zero" and "1" to "HOL.one_class.one".
 INCOMPATIBILITY.
 
 * Added theory Code_Generator providing class 'eq', allowing for code
@@ -737,12 +746,12 @@
 "A = B" (with priority 50).
 
 * Renamed constants in HOL.thy and Orderings.thy:
-    op +   ~> HOL.plus
-    op -   ~> HOL.minus
-    uminus ~> HOL.uminus
-    op *   ~> HOL.times
-    op <   ~> Orderings.less
-    op <=  ~> Orderings.less_eq
+    op +   ~> HOL.plus_class.plus
+    op -   ~> HOL.minus_class.minus
+    uminus ~> HOL.minus_class.uminus
+    op *   ~> HOL.times_class.times
+    op <   ~> Orderings.ord_class.less
+    op <=  ~> Orderings.ord_class.less_eq
 
 Adaptions may be required in the following cases:
 
@@ -763,7 +772,8 @@
 
 d) ML code directly refering to constant names
 This in general only affects hand-written proof tactics, simprocs and so on.
-INCOMPATIBILITY: grep your sourcecode and replace names.
+INCOMPATIBILITY: grep your sourcecode and replace names.  Consider use
+of const_name ML antiquotations.
 
 * Relations less (<) and less_eq (<=) are also available on type bool.
 Modified syntax to disallow nesting without explicit parentheses,
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Algebra/abstract/Ring2.thy
--- a/src/HOL/Algebra/abstract/Ring2.thy	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Algebra/abstract/Ring2.thy	Thu May 17 19:49:40 2007 +0200
@@ -217,7 +217,8 @@
 ML {*
 fun ring_ord (Const (a, _)) =
     find_index (fn a' => a = a')
-      ["HOL.zero", "HOL.plus", "HOL.uminus", "HOL.minus", "HOL.one", "HOL.times"]
+      [@{const_name HOL.zero}, @{const_name HOL.plus}, @{const_name HOL.uminus},
+        @{const_name HOL.minus}, @{const_name HOL.one}, @{const_name HOL.times}]
   | ring_ord _ = ~1;
 
 fun termless_ring (a, b) = (Term.term_lpo ring_ord (a, b) = LESS);
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Hoare/hoare.ML
--- a/src/HOL/Hoare/hoare.ML	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Hoare/hoare.ML	Thu May 17 19:49:40 2007 +0200
@@ -65,7 +65,7 @@
 fun mk_CollectC trm = let val T as Type ("fun",[t,_]) = fastype_of trm 
                       in Collect_const t $ trm end;
 
-fun inclt ty = Const ("Orderings.less_eq", [ty,ty] ---> boolT);
+fun inclt ty = Const (@{const_name Orderings.less_eq}, [ty,ty] ---> boolT);
 
 (** Makes "Mset <= t" **)
 fun Mset_incl t = let val MsetT = fastype_of t 
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Hoare/hoareAbort.ML
--- a/src/HOL/Hoare/hoareAbort.ML	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Hoare/hoareAbort.ML	Thu May 17 19:49:40 2007 +0200
@@ -66,7 +66,7 @@
 fun mk_CollectC trm = let val T as Type ("fun",[t,_]) = fastype_of trm 
                       in Collect_const t $ trm end;
 
-fun inclt ty = Const ("Orderings.less_eq", [ty,ty] ---> boolT);
+fun inclt ty = Const (@{const_name Orderings.less_eq}, [ty,ty] ---> boolT);
 
 (** Makes "Mset <= t" **)
 fun Mset_incl t = let val MsetT = fastype_of t 
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Hyperreal/NSA.thy	Thu May 17 19:49:40 2007 +0200
@@ -671,13 +671,13 @@
   0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
 fun reorient_proc sg _ (_ $ t $ u) =
   case u of
-      Const("HOL.zero", _) => NONE
-    | Const("HOL.one", _) => NONE
-    | Const("Numeral.number_of", _) $ _ => NONE
+      Const(@{const_name HOL.zero}, _) => NONE
+    | Const(@{const_name HOL.one}, _) => NONE
+    | Const(@{const_name Numeral.number_of}, _) $ _ => NONE
     | _ => SOME (case t of
-                Const("HOL.zero", _) => meta_zero_approx_reorient
-              | Const("HOL.one", _) => meta_one_approx_reorient
-              | Const("Numeral.number_of", _) $ _ =>
+                Const(@{const_name HOL.zero}, _) => meta_zero_approx_reorient
+              | Const(@{const_name HOL.one}, _) => meta_one_approx_reorient
+              | Const(@{const_name Numeral.number_of}, _) $ _ =>
                                  meta_number_of_approx_reorient);
 
 in
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Import/Generate-HOL/GenHOL4Base.thy
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Thu May 17 19:49:40 2007 +0200
@@ -166,7 +166,7 @@
 import_theory prim_rec;
 
 const_maps
-    "<" > "Orderings.less" :: "[nat,nat]=>bool";
+    "<" > Orderings.ord_class.less :: "[nat,nat]=>bool";
 
 end_import;
 
@@ -181,15 +181,15 @@
   ">"          > HOL4Compat.nat_gt
   ">="         > HOL4Compat.nat_ge
   FUNPOW       > HOL4Compat.FUNPOW
-  "<="         > "Orderings.less_eq" :: "[nat,nat]=>bool"
-  "+"          > "HOL.plus"       :: "[nat,nat]=>nat"
-  "*"          > "HOL.times"      :: "[nat,nat]=>nat"
-  "-"          > "HOL.minus"      :: "[nat,nat]=>nat"
+  "<="         > Orderings.ord_class.less_eq :: "[nat,nat]=>bool"
+  "+"          > HOL.plus_class.plus       :: "[nat,nat]=>nat"
+  "*"          > HOL.times_class.times      :: "[nat,nat]=>nat"
+  "-"          > HOL.minus_class.minus      :: "[nat,nat]=>nat"
   MIN          > Orderings.min    :: "[nat,nat]=>nat"
   MAX          > Orderings.max    :: "[nat,nat]=>nat"
-  DIV          > "Divides.div" :: "[nat,nat]=>nat"
-  MOD          > "Divides.mod" :: "[nat,nat]=>nat"
-  EXP          > Nat.power        :: "[nat,nat]=>nat";
+  DIV          > Divides.div_class.div :: "[nat,nat]=>nat"
+  MOD          > Divides.div_class.mod :: "[nat,nat]=>nat"
+  EXP          > Nat.power_class.power :: "[nat,nat]=>nat";
 
 end_import;
 
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Import/Generate-HOL/GenHOL4Real.thy
--- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Thu May 17 19:49:40 2007 +0200
@@ -23,7 +23,7 @@
   inv      > HOL.inverse :: "real => real"
   real_add > HOL.plus    :: "[real,real] => real"
   real_mul > HOL.times   :: "[real,real] => real"
-  real_lt  > "Orderings.less"      :: "[real,real] => bool";
+  real_lt  > Orderings.ord_class.less :: "[real,real] => bool";
 
 ignore_thms
     real_TY_DEF
@@ -51,7 +51,7 @@
 const_maps
   real_gt     > HOL4Compat.real_gt
   real_ge     > HOL4Compat.real_ge
-  real_lte    > Orderings.less_eq :: "[real,real] => bool"
+  real_lte    > Orderings.ord_class.less_eq :: "[real,real] => bool"
   real_sub    > HOL.minus    :: "[real,real] => real"
   "/"         > HOL.divide   :: "[real,real] => real"
   pow         > Nat.power    :: "[real,nat] => real"
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Import/HOL/arithmetic.imp
--- a/src/HOL/Import/HOL/arithmetic.imp	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Import/HOL/arithmetic.imp	Thu May 17 19:49:40 2007 +0200
@@ -14,19 +14,19 @@
   "NUMERAL_BIT2" > "HOL4Compat.NUMERAL_BIT2"
   "NUMERAL_BIT1" > "HOL4Compat.NUMERAL_BIT1"
   "NUMERAL" > "HOL4Compat.NUMERAL"
-  "MOD" > "Divides.mod" :: "nat => nat => nat"
   "MIN" > "Orderings.min" :: "nat => nat => nat"
   "MAX" > "Orderings.max" :: "nat => nat => nat"
   "FUNPOW" > "HOL4Compat.FUNPOW"
-  "EXP" > "Nat.power" :: "nat => nat => nat"
-  "DIV" > "Divides.div" :: "nat => nat => nat"
+  "EXP" > "Nat.power_class.power" :: "nat => nat => nat"
+  "DIV" > "Divides.div_class.div" :: "nat => nat => nat"
+  "MOD" > "Divides.div_class.mod" :: "nat => nat => nat"
   "ALT_ZERO" > "HOL4Compat.ALT_ZERO"
   ">=" > "HOL4Compat.nat_ge"
   ">" > "HOL4Compat.nat_gt"
-  "<=" > "Orderings.less_eq" :: "nat => nat => bool"
-  "-" > "HOL.minus" :: "nat => nat => nat"
-  "+" > "HOL.plus" :: "nat => nat => nat"
-  "*" > "HOL.times" :: "nat => nat => nat"
+  "<=" > "Orderings.ord_class.less_eq" :: "nat => nat => bool"
+  "-" > "HOL.minus_class.minus" :: "nat => nat => nat"
+  "+" > "HOL.plus_class.plus" :: "nat => nat => nat"
+  "*" > "HOL.times_class.times" :: "nat => nat => nat"
 
 thm_maps
   "num_case_def" > "HOL4Compat.num_case_def"
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Import/HOL/list.imp
--- a/src/HOL/Import/HOL/list.imp	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Import/HOL/list.imp	Thu May 17 19:49:40 2007 +0200
@@ -22,7 +22,7 @@
   "MEM" > "List.op mem"
   "MAP2" > "HOL4Compat.map2"
   "MAP" > "List.map"
-  "LENGTH" > "Nat.size"
+  "LENGTH" > "Nat.size_class.size"
   "LAST" > "List.last"
   "HD" > "List.hd"
   "FRONT" > "List.butlast"
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Import/HOL/prim_rec.imp
--- a/src/HOL/Import/HOL/prim_rec.imp	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Import/HOL/prim_rec.imp	Thu May 17 19:49:40 2007 +0200
@@ -18,7 +18,7 @@
   "PRIM_REC_FUN" > "HOL4Base.prim_rec.PRIM_REC_FUN"
   "PRIM_REC" > "HOL4Base.prim_rec.PRIM_REC"
   "PRE" > "HOL4Base.prim_rec.PRE"
-  "<" > "Orderings.less" :: "nat => nat => bool"
+  "<" > "Orderings.ord_class.less" :: "nat => nat => bool"
 
 thm_maps
   "wellfounded_primdef" > "HOL4Base.prim_rec.wellfounded_primdef"
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Import/HOL/real.imp
--- a/src/HOL/Import/HOL/real.imp	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Import/HOL/real.imp	Thu May 17 19:49:40 2007 +0200
@@ -10,14 +10,14 @@
 const_maps
   "sup" > "HOL4Real.real.sup"
   "sum" > "HOL4Real.real.sum"
-  "real_sub" > "HOL.minus" :: "real => real => real"
+  "real_sub" > "HOL.minus_class.minus" :: "real => real => real"
   "real_of_num" > "RealDef.real" :: "nat => real"
-  "real_lte" > "Orderings.less_eq" :: "real => real => bool"
+  "real_lte" > "Orderings.ord_class.less_eq" :: "real => real => bool"
   "real_gt" > "HOL4Compat.real_gt"
   "real_ge" > "HOL4Compat.real_ge"
-  "pow" > "Nat.power" :: "real => nat => real"
-  "abs" > "HOL.abs" :: "real => real"
-  "/" > "HOL.divide" :: "real => real => real"
+  "pow" > "Nat.power_class.power" :: "real => nat => real"
+  "abs" > "HOL.minus_class.abs" :: "real => real"
+  "/" > "HOL.divides_class.divide" :: "real => real => real"
 
 thm_maps
   "sup_def" > "HOL4Real.real.sup_def"
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Import/HOL/realax.imp
--- a/src/HOL/Import/HOL/realax.imp	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Import/HOL/realax.imp	Thu May 17 19:49:40 2007 +0200
@@ -27,13 +27,13 @@
   "treal_add" > "HOL4Real.realax.treal_add"
   "treal_1" > "HOL4Real.realax.treal_1"
   "treal_0" > "HOL4Real.realax.treal_0"
-  "real_neg" > "HOL.uminus" :: "real => real"
-  "real_mul" > "HOL.times" :: "real => real => real"
-  "real_lt" > "Orderings.less" :: "real => real => bool"
-  "real_add" > "HOL.plus" :: "real => real => real"
-  "real_1" > "1" :: "real"
-  "real_0" > "0" :: "real"
-  "inv" > "HOL.inverse" :: "real => real"
+  "real_neg" > "HOL.minus_class.uminus" :: "real => real"
+  "real_mul" > "HOL.times_class.times" :: "real => real => real"
+  "real_lt" > "Orderings.ord_class.less" :: "real => real => bool"
+  "real_add" > "HOL.plus_class.plus" :: "real => real => real"
+  "real_1" > "HOL.one_class.one" :: "real"
+  "real_0" > "HOL.zero_class.zero" :: "real"
+  "inv" > "HOL.divide_class.inverse" :: "real => real"
   "hreal_of_treal" > "HOL4Real.realax.hreal_of_treal"
 
 thm_maps
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Import/HOLLight/hollight.imp
--- a/src/HOL/Import/HOLLight/hollight.imp	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Import/HOLLight/hollight.imp	Thu May 17 19:49:40 2007 +0200
@@ -238,10 +238,10 @@
   "<=" > "HOLLight.hollight.<="
   "<" > "HOLLight.hollight.<"
   "/\\" > "op &"
-  "-" > "HOL.minus" :: "nat => nat => nat"
+  "-" > "HOL.minus_class.minus" :: "nat => nat => nat"
   "," > "Pair"
-  "+" > "HOL.plus" :: "nat => nat => nat"
-  "*" > "HOL.times" :: "nat => nat => nat"
+  "+" > "HOL.plus_class.plus" :: "nat => nat => nat"
+  "*" > "HOL.times_class.times" :: "nat => nat => nat"
   "$" > "HOLLight.hollight.$"
   "!" > "All"
 
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Integ/IntArith.thy
--- a/src/HOL/Integ/IntArith.thy	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Integ/IntArith.thy	Thu May 17 19:49:40 2007 +0200
@@ -7,7 +7,7 @@
 
 theory IntArith
 imports Numeral "../Wellfounded_Relations"
-uses ("int_arith1.ML")
+uses "~~/src/Provers/Arith/assoc_fold.ML" ("int_arith1.ML")
 begin
 
 text{*Duplicate: can't understand why it's necessary*}
@@ -103,7 +103,6 @@
  max_def[of "number_of u" "1::int", standard, simp]
  min_def[of "number_of u" "1::int", standard, simp]
 
-
 use "int_arith1.ML"
 setup int_arith_setup
 
@@ -394,7 +393,7 @@
 done
 
 
-subsection {* Legavy ML bindings *}
+subsection {* Legacy ML bindings *}
 
 ML {*
 val of_int_number_of_eq = @{thm of_int_number_of_eq};
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Integ/Numeral.thy
--- a/src/HOL/Integ/Numeral.thy	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Integ/Numeral.thy	Thu May 17 19:49:40 2007 +0200
@@ -8,7 +8,7 @@
 
 theory Numeral
 imports IntDef
-uses "../Tools/numeral_syntax.ML"
+uses ("../Tools/numeral_syntax.ML")
 begin
 
 subsection {* Binary representation *}
@@ -50,6 +50,7 @@
 syntax
   "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")
 
+use "../Tools/numeral_syntax.ML"
 setup NumeralSyntax.setup
 
 abbreviation
@@ -648,14 +649,14 @@
 setup {*
 let
 
-fun number_of_codegen thy defs gr dep module b (Const ("Numeral.number_of", Type ("fun", [_, T])) $ t) =
+fun number_of_codegen thy defs gr dep module b (Const (@{const_name Numeral.number_of}, Type ("fun", [_, T])) $ t) =
       if T = HOLogic.intT then
         (SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, T)),
           (Pretty.str o IntInf.toString o HOLogic.dest_numeral) t) handle TERM _ => NONE)
       else if T = HOLogic.natT then
         SOME (Codegen.invoke_codegen thy defs dep module b (gr,
           Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT) $
-            (Const ("Numeral.number_of", HOLogic.intT --> HOLogic.intT) $ t)))
+            (Const (@{const_name Numeral.number_of}, HOLogic.intT --> HOLogic.intT) $ t)))
       else NONE
   | number_of_codegen _ _ _ _ _ _ _ = NONE;
 
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Integ/cooper_dec.ML
--- a/src/HOL/Integ/cooper_dec.ML	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Integ/cooper_dec.ML	Thu May 17 19:49:40 2007 +0200
@@ -10,12 +10,12 @@
 signature COOPER_DEC = 
 sig
   exception COOPER
-  val is_arith_rel : term -> bool
   val mk_number : IntInf.int -> term
-  val dest_number : term -> IntInf.int
-  val is_numeral : term -> bool
   val zero : term
   val one : term
+  val dest_number : term -> IntInf.int
+  val is_number : term -> bool
+  val is_arith_rel : term -> bool
   val linear_cmul : IntInf.int -> term -> term
   val linear_add : string list -> term -> term -> term 
   val linear_sub : string list -> term -> term -> term 
@@ -74,20 +74,13 @@
 (*Function is_arith_rel returns true if and only if the term is an operation of the 
 form [int,int]---> int*) 
  
-(*Transform a natural (FIXME?) number to a term*) 
-val mk_number = HOLogic.mk_number HOLogic.intT
- 
-(*Transform an Term to an natural (FIXME?) number*)
+val mk_number = HOLogic.mk_number HOLogic.intT;
+val zero = mk_number 0; 
+val one = mk_number 1; 
 fun dest_number t = let
     val (T, n) = HOLogic.dest_number t
   in if T = HOLogic.intT then n else error ("bad typ: " ^ Display.raw_string_of_typ T) end;
-
-(*Some terms often used for pattern matching*) 
-val zero = mk_number 0; 
-val one = mk_number 1; 
-
-(*Tests if a Term is representing a number*) 
-val is_numeral = can dest_number; 
+val is_number = can dest_number; 
 
 (*maps a unary natural function on a term containing an natural number*) 
 fun numeral1 f n = mk_number (f (dest_number n)); 
@@ -106,8 +99,8 @@
  
 fun linear_cmul n tm =  if n = 0 then zero else let fun times n k = n*k in  
   ( case tm of  
-     (Const("HOL.plus",T)  $  (Const ("HOL.times",T1 ) $c1 $  x1) $ rest) => 
-       Const("HOL.plus",T) $ ((Const("HOL.times",T1) $ (numeral1 (times n) c1) $ x1)) $ (linear_cmul n rest) 
+     (Const(@{const_name HOL.plus},T)  $  (Const (@{const_name HOL.times},T1 ) $c1 $  x1) $ rest) => 
+       Const(@{const_name HOL.plus},T) $ ((Const(@{const_name HOL.times},T1) $ (numeral1 (times n) c1) $ x1)) $ (linear_cmul n rest) 
     |_ =>  numeral1 (times n) tm) 
     end ; 
  
@@ -129,23 +122,23 @@
 fun linear_add vars tm1 tm2 = 
   let fun addwith x y = x + y in
  (case (tm1,tm2) of 
-	((Const ("HOL.plus",T1) $ ( Const("HOL.times",T2) $ c1 $  x1) $ rest1),(Const 
-	("HOL.plus",T3)$( Const("HOL.times",T4) $ c2 $  x2) $ rest2)) => 
+	((Const (@{const_name HOL.plus},T1) $ ( Const(@{const_name HOL.times},T2) $ c1 $  x1) $ rest1),(Const 
+	(@{const_name HOL.plus},T3)$( Const(@{const_name HOL.times},T4) $ c2 $  x2) $ rest2)) => 
          if x1 = x2 then 
               let val c = (numeral2 (addwith) c1 c2) 
 	      in 
               if c = zero then (linear_add vars rest1  rest2)  
-	      else (Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c $ x1) $ (linear_add vars  rest1 rest2)) 
+	      else (Const(@{const_name HOL.plus},T1) $ (Const(@{const_name HOL.times},T2) $ c $ x1) $ (linear_add vars  rest1 rest2)) 
               end 
 	   else 
-		if earlierv vars x1 x2 then (Const("HOL.plus",T1) $  
-		(Const("HOL.times",T2)$ c1 $ x1) $ (linear_add vars rest1 tm2)) 
-    	       else (Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c2 $ x2) $ (linear_add vars tm1 rest2)) 
-   	|((Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c1 $ x1) $ rest1) ,_) => 
-    	  (Const("HOL.plus",T1)$ (Const("HOL.times",T2) $ c1 $ x1) $ (linear_add vars 
+		if earlierv vars x1 x2 then (Const(@{const_name HOL.plus},T1) $  
+		(Const(@{const_name HOL.times},T2)$ c1 $ x1) $ (linear_add vars rest1 tm2)) 
+    	       else (Const(@{const_name HOL.plus},T1) $ (Const(@{const_name HOL.times},T2) $ c2 $ x2) $ (linear_add vars tm1 rest2)) 
+   	|((Const(@{const_name HOL.plus},T1) $ (Const(@{const_name HOL.times},T2) $ c1 $ x1) $ rest1) ,_) => 
+    	  (Const(@{const_name HOL.plus},T1)$ (Const(@{const_name HOL.times},T2) $ c1 $ x1) $ (linear_add vars 
 	  rest1 tm2)) 
-   	|(_, (Const("HOL.plus",T1) $(Const("HOL.times",T2) $ c2 $ x2) $ rest2)) => 
-      	  (Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c2 $ x2) $ (linear_add vars tm1 
+   	|(_, (Const(@{const_name HOL.plus},T1) $(Const(@{const_name HOL.times},T2) $ c2 $ x2) $ rest2)) => 
+      	  (Const(@{const_name HOL.plus},T1) $ (Const(@{const_name HOL.times},T2) $ c2 $ x2) $ (linear_add vars tm1 
 	  rest2)) 
    	| (_,_) => numeral2 (addwith) tm1 tm2) 
 	 
@@ -169,19 +162,19 @@
  c*Free(x,T) + t where c is a constant ant t is a Term which is not containing 
  Free(x,T)*) 
   
-fun lint vars tm = if is_numeral tm then tm else case tm of 
-   (Free (x,T)) =>  (HOLogic.mk_binop "HOL.plus" ((HOLogic.mk_binop "HOL.times" ((mk_number 1),Free (x,T))), zero)) 
-  |(Bound i) =>  (Const("HOL.plus",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ 
-  (Const("HOL.times",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_number 1) $ (Bound i)) $ zero) 
-  |(Const("HOL.uminus",_) $ t ) => (linear_neg (lint vars t)) 
-  |(Const("HOL.plus",_) $ s $ t) => (linear_add vars (lint vars s) (lint vars t)) 
-  |(Const("HOL.minus",_) $ s $ t) => (linear_sub vars (lint vars s) (lint vars t)) 
-  |(Const ("HOL.times",_) $ s $ t) => 
+fun lint vars tm = if is_number tm then tm else case tm of 
+   (Free (x,T)) =>  (HOLogic.mk_binop @{const_name HOL.plus} ((HOLogic.mk_binop @{const_name HOL.times} ((mk_number 1),Free (x,T))), zero)) 
+  |(Bound i) =>  (Const(@{const_name HOL.plus},HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ 
+  (Const(@{const_name HOL.times},HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_number 1) $ (Bound i)) $ zero) 
+  |(Const(@{const_name HOL.uminus},_) $ t ) => (linear_neg (lint vars t)) 
+  |(Const(@{const_name HOL.plus},_) $ s $ t) => (linear_add vars (lint vars s) (lint vars t)) 
+  |(Const(@{const_name HOL.minus},_) $ s $ t) => (linear_sub vars (lint vars s) (lint vars t)) 
+  |(Const (@{const_name HOL.times},_) $ s $ t) => 
         let val s' = lint vars s  
             val t' = lint vars t  
         in 
-        if is_numeral s' then (linear_cmul (dest_number s') t') 
-        else if is_numeral t' then (linear_cmul (dest_number t') s') 
+        if is_number s' then (linear_cmul (dest_number s') t') 
+        else if is_number t' then (linear_cmul (dest_number t') s') 
  
          else raise COOPER
          end 
@@ -196,20 +189,20 @@
 fun mkatom vars p t = Const(p,HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ zero $ (lint vars t); 
  
 fun linform vars (Const ("Divides.dvd",_) $ c $ t) =
-    if is_numeral c then   
+    if is_number c then   
       let val c' = (mk_number(abs(dest_number c)))  
       in (HOLogic.mk_binrel "Divides.dvd" (c,lint vars t)) 
       end 
     else (warning "Nonlinear term --- Non numeral leftside at dvd"
       ;raise COOPER)
-  |linform vars  (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ s $ t ) = (mkatom vars "op =" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s) ) 
-  |linform vars  (Const("Orderings.less",_)$ s $t ) = (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s))
-  |linform vars  (Const("op >",_) $ s $ t ) = (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t)) 
-  |linform vars  (Const("Orderings.less_eq",_)$ s $ t ) = 
-        (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_number 1)) $ s)) 
+  |linform vars  (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ s $ t ) = (mkatom vars "op =" (Const (@{const_name HOL.minus},HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s) ) 
+  |linform vars  (Const(@{const_name Orderings.less},_)$ s $t ) = (mkatom vars @{const_name Orderings.less} (Const (@{const_name HOL.minus},HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s))
+  |linform vars  (Const("op >",_) $ s $ t ) = (mkatom vars @{const_name Orderings.less} (Const (@{const_name HOL.minus},HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t)) 
+  |linform vars  (Const(@{const_name Orderings.less_eq},_)$ s $ t ) = 
+        (mkatom vars @{const_name Orderings.less} (Const (@{const_name HOL.minus},HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const(@{const_name HOL.plus},HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_number 1)) $ s)) 
   |linform vars  (Const("op >=",_)$ s $ t ) = 
-        (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> 
-	HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> 
+        (mkatom vars @{const_name Orderings.less} (Const (@{const_name HOL.minus},HOLogic.intT --> HOLogic.intT --> 
+	HOLogic.intT) $ (Const(@{const_name HOL.plus},HOLogic.intT --> HOLogic.intT --> 
 	HOLogic.intT) $s $(mk_number 1)) $ t)) 
  
    |linform vars  fm =  fm; 
@@ -219,8 +212,8 @@
 (* ------------------------------------------------------------------------- *) 
  
 fun posineq fm = case fm of  
- (Const ("Not",_)$(Const("Orderings.less",_)$ c $ t)) =>
-   (HOLogic.mk_binrel "Orderings.less"  (zero , (linear_sub [] (mk_number 1) (linear_add [] c t ) ))) 
+ (Const ("Not",_)$(Const(@{const_name Orderings.less},_)$ c $ t)) =>
+   (HOLogic.mk_binrel @{const_name Orderings.less}  (zero , (linear_sub [] (mk_number 1) (linear_add [] c t ) ))) 
   | ( Const ("op &",_) $ p $ q)  => HOLogic.mk_conj (posineq p,posineq q)
   | ( Const ("op |",_) $ p $ q ) => HOLogic.mk_disj (posineq p,posineq q)
   | _ => fm; 
@@ -236,7 +229,7 @@
 fun lcm_num a b = (abs a*b) div (gcd (abs a) (abs b)); 
  
 fun formlcm x fm = case fm of 
-    (Const (p,_)$ _ $(Const ("HOL.plus", _)$(Const ("HOL.times",_)$ c $ y ) $z ) ) =>  if 
+    (Const (p,_)$ _ $(Const (@{const_name HOL.plus}, _)$(Const (@{const_name HOL.times},_)$ c $ y ) $z ) ) =>  if 
     (is_arith_rel fm) andalso (x = y) then  (abs(dest_number c)) else 1 
   | ( Const ("Not", _) $p) => formlcm x p 
   | ( Const ("op &",_) $ p $ q) => lcm_num (formlcm x p) (formlcm x q) 
@@ -249,13 +242,13 @@
  
 fun adjustcoeff x l fm = 
      case fm of  
-      (Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $ 
+      (Const(p,_) $d $( Const (@{const_name HOL.plus}, _)$(Const (@{const_name HOL.times},_) $ 
       c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then  
         let val m = l div (dest_number c) 
-            val n = (if p = "Orderings.less" then abs(m) else m) 
-            val xtm = HOLogic.mk_binop "HOL.times" ((mk_number (m div n)), x) 
+            val n = (if p = @{const_name Orderings.less} then abs(m) else m) 
+            val xtm = HOLogic.mk_binop @{const_name HOL.times} ((mk_number (m div n)), x) 
 	in
-        (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) )))) 
+        (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop @{const_name HOL.plus} ( xtm ,( linear_cmul n z) )))) 
 	end 
 	else fm 
   |( Const ("Not", _) $ p) => HOLogic.Not $ (adjustcoeff x l p) 
@@ -272,8 +265,8 @@
       val fm' = adjustcoeff x l fm in
       if l = 1 then fm' 
 	 else 
-     let val xp = (HOLogic.mk_binop "HOL.plus"  
-     		((HOLogic.mk_binop "HOL.times" ((mk_number 1), x )), zero))
+     let val xp = (HOLogic.mk_binop @{const_name HOL.plus}  
+     		((HOLogic.mk_binop @{const_name HOL.times} ((mk_number 1), x )), zero))
 	in 
       HOLogic.conj $(HOLogic.mk_binrel "Divides.dvd" ((mk_number l) , xp )) $ (adjustcoeff x l fm) 
       end 
@@ -284,12 +277,12 @@
 (*
 fun adjustcoeffeq x l fm = 
     case fm of  
-      (Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $ 
+      (Const(p,_) $d $( Const (@{const_name HOL.plus}, _)$(Const (@{const_name HOL.times},_) $ 
       c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then  
         let val m = l div (dest_number c) 
-            val n = (if p = "Orderings.less" then abs(m) else m)  
-            val xtm = (HOLogic.mk_binop "HOL.times" ((mk_number ((m div n)*l) ), x))
-            in (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) )))) 
+            val n = (if p = @{const_name Orderings.less} then abs(m) else m)  
+            val xtm = (HOLogic.mk_binop @{const_name HOL.times} ((mk_number ((m div n)*l) ), x))
+            in (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop @{const_name HOL.plus} ( xtm ,( linear_cmul n z) )))) 
 	    end 
 	else fm 
   |( Const ("Not", _) $ p) => HOLogic.Not $ (adjustcoeffeq x l p) 
@@ -305,11 +298,11 @@
 (* ------------------------------------------------------------------------- *) 
  
 fun minusinf x fm = case fm of  
-    (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) => 
+    (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) => 
   	 if (is_arith_rel fm) andalso (x=y) andalso (c2 = one) andalso (c1 =zero) then HOLogic.false_const  
 	 				 else fm 
  
-  |(Const("Orderings.less",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z 
+  |(Const(@{const_name Orderings.less},_) $ c $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z 
   )) => if (x = y) 
 	then if (pm1 = one) andalso (c = zero) then HOLogic.false_const 
 	     else if (dest_number pm1 = ~1) andalso (c = zero) then HOLogic.true_const 
@@ -326,11 +319,11 @@
 (* ------------------------------------------------------------------------- *)
 
 fun plusinf x fm = case fm of
-    (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
+    (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
   	 if (is_arith_rel fm) andalso (x=y) andalso (c2 = one) andalso (c1 =zero) then HOLogic.false_const
 	 				 else fm
 
-  |(Const("Orderings.less",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z
+  |(Const(@{const_name Orderings.less},_) $ c $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z
   )) => if (x = y) 
 	then if (pm1 = one) andalso (c = zero) then HOLogic.true_const 
 	     else if (dest_number pm1 = ~1) andalso (c = zero) then HOLogic.false_const
@@ -346,7 +339,7 @@
 (* The LCM of all the divisors that involve x.                               *) 
 (* ------------------------------------------------------------------------- *) 
  
-fun divlcm x (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z ) ) =  
+fun divlcm x (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z ) ) =  
         if x = y then abs(dest_number d) else 1 
   |divlcm x ( Const ("Not", _) $ p) = divlcm x p 
   |divlcm x ( Const ("op &",_) $ p $ q) = lcm_num (divlcm x p) (divlcm x q) 
@@ -360,15 +353,15 @@
 fun bset x fm = case fm of 
    (Const ("Not", _) $ p) => if (is_arith_rel p) then  
           (case p of  
-	      (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $c2 $y) $a ) )  
+	      (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $c2 $y) $a ) )  
 	             => if (is_arith_rel p) andalso (x=	y) andalso (c2 = one) andalso (c1 = zero)  
 	                then [linear_neg a] 
 			else  bset x p 
    	  |_ =>[]) 
 			 
 			else bset x p 
-  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_number 1))]  else [] 
-  |(Const ("Orderings.less",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else [] 
+  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_number 1))]  else [] 
+  |(Const (@{const_name Orderings.less},_) $ c1$ (Const (@{const_name HOL.plus},_) $(Const (@{const_name HOL.times},_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else [] 
   |(Const ("op &",_) $ p $ q) => (bset x p) union (bset x q) 
   |(Const ("op |",_) $ p $ q) => (bset x p) union (bset x q) 
   |_ => []; 
@@ -380,15 +373,15 @@
 fun aset x fm = case fm of
    (Const ("Not", _) $ p) => if (is_arith_rel p) then
           (case p of
-	      (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $c2 $y) $a ) )
+	      (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $c2 $y) $a ) )
 	             => if (x=	y) andalso (c2 = one) andalso (c1 = zero)
 	                then [linear_neg a]
 			else  []
    	  |_ =>[])
 
 			else aset x p
-  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_number 1) a]  else []
-  |(Const ("Orderings.less",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_number (~1))) then [a] else []
+  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_number 1) a]  else []
+  |(Const (@{const_name Orderings.less},_) $ c1$ (Const (@{const_name HOL.plus},_) $(Const (@{const_name HOL.times},_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_number (~1))) then [a] else []
   |(Const ("op &",_) $ p $ q) => (aset x p) union (aset x q)
   |(Const ("op |",_) $ p $ q) => (aset x p) union (aset x q)
   |_ => [];
@@ -399,7 +392,7 @@
 (* ------------------------------------------------------------------------- *) 
  
 fun linrep vars x t fm = case fm of  
-   ((Const(p,_)$ d $ (Const("HOL.plus",_)$(Const("HOL.times",_)$ c $ y) $ z))) => 
+   ((Const(p,_)$ d $ (Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$ c $ y) $ z))) => 
       if (x = y) andalso (is_arith_rel fm)  
       then  
         let val ct = linear_cmul (dest_number c) t  
@@ -420,18 +413,18 @@
 exception DVD_UNKNOWN
 
 fun dvd_op (d, t) = 
- if not(is_numeral d) then raise DVD_UNKNOWN
+ if not(is_number d) then raise DVD_UNKNOWN
  else let 
    val dn = dest_number d
    fun coeffs_of x = case x of 
      Const(p,_) $ tl $ tr => 
-       if p = "HOL.plus" then (coeffs_of tl) union (coeffs_of tr)
-          else if p = "HOL.times" 
-	        then if (is_numeral tr) 
+       if p = @{const_name HOL.plus} then (coeffs_of tl) union (coeffs_of tr)
+          else if p = @{const_name HOL.times} 
+	        then if (is_number tr) 
 		 then [(dest_number tr) * (dest_number tl)] 
 		 else [dest_number tl]
 	        else []
-    |_ => if (is_numeral t) then [dest_number t]  else []
+    |_ => if (is_number t) then [dest_number t]  else []
    val ts = coeffs_of t
    in case ts of
      [] => raise DVD_UNKNOWN
@@ -440,7 +433,7 @@
 
 
 val operations = 
-  [("op =",op=), ("Orderings.less",IntInf.<), ("op >",IntInf.>), ("Orderings.less_eq",IntInf.<=) , 
+  [("op =",op=), (@{const_name Orderings.less},IntInf.<), ("op >",IntInf.>), (@{const_name Orderings.less_eq},IntInf.<=) , 
    ("op >=",IntInf.>=), 
    ("Divides.dvd",fn (x,y) =>((IntInf.mod(y, x)) = 0))]; 
  
@@ -648,8 +641,8 @@
     |mk_uni_vars T (Free (v,_)) = Free (v,T) 
     |mk_uni_vars T tm = tm; 
  
-fun mk_uni_int T (Const ("HOL.zero",T2)) = if T = T2 then (mk_number 0) else (Const ("HOL.zero",T2)) 
-    |mk_uni_int T (Const ("HOL.one",T2)) = if T = T2 then (mk_number 1) else (Const ("HOL.one",T2)) 
+fun mk_uni_int T (Const (@{const_name HOL.zero},T2)) = if T = T2 then (mk_number 0) else (Const (@{const_name HOL.zero},T2)) 
+    |mk_uni_int T (Const (@{const_name HOL.one},T2)) = if T = T2 then (mk_number 1) else (Const (@{const_name HOL.one},T2)) 
     |mk_uni_int T (node $ rest) = (mk_uni_int T node) $ (mk_uni_int T rest )  
     |mk_uni_int T (Abs(AV,AT,p)) = Abs(AV,AT,mk_uni_int T p) 
     |mk_uni_int T tm = tm; 
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Integ/cooper_proof.ML
--- a/src/HOL/Integ/cooper_proof.ML	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Integ/cooper_proof.ML	Thu May 17 19:49:40 2007 +0200
@@ -155,17 +155,17 @@
 
 (* ------------------------------------------------------------------------- *)
 (*This function norm_zero_one  replaces the occurences of Numeral1 and Numeral0*)
-(*Respectively by their abstract representation Const("HOL.one",..) and Const("HOL.zero",..)*)
+(*Respectively by their abstract representation Const(@{const_name HOL.one},..) and Const(@{const_name HOL.zero},..)*)
 (*this is necessary because the theorems use this representation.*)
 (* This function should be elminated in next versions...*)
 (* ------------------------------------------------------------------------- *)
 
 fun norm_zero_one fm = case fm of
-  (Const ("HOL.times",_) $ c $ t) => 
+  (Const (@{const_name HOL.times},_) $ c $ t) => 
     if c = one then (norm_zero_one t)
     else if (dest_number c = ~1) 
-         then (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $ (norm_zero_one t))
-         else (HOLogic.mk_binop "HOL.times" (norm_zero_one c,norm_zero_one t))
+         then (Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $ (norm_zero_one t))
+         else (HOLogic.mk_binop @{const_name HOL.times} (norm_zero_one c,norm_zero_one t))
   |(node $ rest) => ((norm_zero_one node)$(norm_zero_one rest))
   |(Abs(x,T,p)) => (Abs(x,T,(norm_zero_one p)))
   |_ => fm;
@@ -251,32 +251,32 @@
 (*==================================================*)
 
 fun decomp_adjustcoeffeq sg x l fm = case fm of
-    (Const("Not",_)$(Const("Orderings.less",_) $(Const("HOL.zero",_)) $(rt as (Const ("HOL.plus", _)$(Const ("HOL.times",_) $    c $ y ) $z )))) => 
+    (Const("Not",_)$(Const(@{const_name Orderings.less},_) $ zero $(rt as (Const (@{const_name HOL.plus}, _)$(Const (@{const_name HOL.times},_) $    c $ y ) $z )))) => 
      let  
         val m = l div (dest_number c) 
         val n = if (x = y) then abs (m) else 1
-        val xtm = (HOLogic.mk_binop "HOL.times" ((mk_number ((m div n)*l) ), x)) 
+        val xtm = (HOLogic.mk_binop @{const_name HOL.times} ((mk_number ((m div n)*l) ), x)) 
         val rs = if (x = y) 
-                 then (HOLogic.mk_binrel "Orderings.less" (zero,linear_sub [] (mk_number n) (HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) )))) 
-                 else HOLogic.mk_binrel "Orderings.less" (zero,linear_sub [] one rt )
+                 then (HOLogic.mk_binrel @{const_name Orderings.less} (zero,linear_sub [] (mk_number n) (HOLogic.mk_binop @{const_name HOL.plus} ( xtm ,( linear_cmul n z) )))) 
+                 else HOLogic.mk_binrel @{const_name Orderings.less} (zero,linear_sub [] one rt )
         val ck = cterm_of sg (mk_number n)
         val cc = cterm_of sg c
         val ct = cterm_of sg z
         val cx = cterm_of sg y
         val pre = prove_elementar sg "lf" 
-            (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),(mk_number n)))
+            (HOLogic.mk_binrel @{const_name Orderings.less} (zero, mk_number n))
         val th1 = (pre RS (instantiate' [] [SOME ck,SOME cc, SOME cx, SOME ct] (ac_pi_eq)))
         in ([], fn [] => [th1,(prove_elementar sg "sa" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
         end
 
-  |(Const(p,_) $a $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $ 
+  |(Const(p,_) $a $( Const (@{const_name HOL.plus}, _)$(Const (@{const_name HOL.times},_) $ 
       c $ y ) $t )) => 
    if (is_arith_rel fm) andalso (x = y) 
    then  
         let val m = l div (dest_number c) 
-           val k = (if p = "Orderings.less" then abs(m) else m)  
-           val xtm = (HOLogic.mk_binop "HOL.times" ((mk_number ((m div k)*l) ), x))
-           val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul k t) )))) 
+           val k = (if p = @{const_name Orderings.less} then abs(m) else m)  
+           val xtm = (HOLogic.mk_binop @{const_name HOL.times} ((mk_number ((m div k)*l) ), x))
+           val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop @{const_name HOL.plus} ( xtm ,( linear_cmul k t) )))) 
 
            val ck = cterm_of sg (mk_number k)
            val cc = cterm_of sg c
@@ -286,23 +286,23 @@
 
 	   in 
 	case p of
-	  "Orderings.less" => 
+	  @{const_name Orderings.less} => 
 	let val pre = prove_elementar sg "lf" 
-	    (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),(mk_number k)))
+	    (HOLogic.mk_binrel @{const_name Orderings.less} (zero, mk_number k))
             val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct] (ac_lt_eq)))
 	in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
          end
 
            |"op =" =>
 	     let val pre = prove_elementar sg "lf" 
-	    (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_number k))))
+	    (HOLogic.Not $ (HOLogic.mk_binrel "op =" (zero, mk_number k)))
 	         val th1 = (pre RS(instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct] (ac_eq_eq)))
 	     in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
              end
 
              |"Divides.dvd" =>
 	       let val pre = prove_elementar sg "lf" 
-	   (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_number k))))
+	   (HOLogic.Not $ (HOLogic.mk_binrel "op =" (zero, mk_number k)))
                    val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct]) (ac_dvd_eq))
                in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
                         
@@ -331,31 +331,31 @@
    val cfalse = cterm_of sg HOLogic.false_const
    val fm = norm_zero_one fm1
   in  case fm1 of 
-      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
+      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) => 
          if (x=y) andalso (c1= zero) andalso (c2= one) then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf))
            else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
 
-      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
+      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
   	   if (is_arith_rel fm) andalso (x=y) andalso (c1= zero) andalso (c2= one) 
 	   then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf))
 	 	 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf)) 
 
-      |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+      |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) =>
            if (y=x) andalso (c1 = zero) then 
             if (pm1 = one) then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf)) else
 	     (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf))
 	    else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
   
-      |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+      |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => 
          if y=x then  let val cz = cterm_of sg (norm_zero_one z)
-			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero)
+			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero)
 	 	      in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_minf)))
 		      end
 		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
-      |(Const("Divides.dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
+      |(Const("Divides.dvd",_)$ d $ (db as (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $
       c $ y ) $ z))) => 
          if y=x then  let val cz = cterm_of sg (norm_zero_one z)
-			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero)
+			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero)
 	 	      in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_minf)))
 		      end
 		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
@@ -369,22 +369,22 @@
    let
    val fm = norm_zero_one fm1
     in  case fm1 of 
-      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
+      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) => 
          if  (x=y) andalso (c1=zero) andalso (c2=one) 
 	   then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (neq_eq_minf))
            else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
 
-      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
+      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
   	   if (is_arith_rel fm) andalso (x=y) andalso ((c1=zero) orelse (c1 = norm_zero_one zero)) andalso ((c2=one) orelse (c1 = norm_zero_one one))
 	     then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_minf))
 	     else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf)) 
 
-      |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+      |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) =>
            if (y=x) andalso (c1 =zero) then 
             if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_minf)) else
 	     (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_minf))
 	    else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
-      |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+      |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => 
          if y=x then  let val cd = cterm_of sg (norm_zero_one d)
 	 		  val cz = cterm_of sg (norm_zero_one z)
 	 	      in(instantiate' [] [SOME cd,  SOME cz] (not_dvd_eq_minf)) 
@@ -392,7 +392,7 @@
 
 		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
 		
-      |(Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+      |(Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => 
          if y=x then  let val cd = cterm_of sg (norm_zero_one d)
 	 		  val cz = cterm_of sg (norm_zero_one z)
 	 	      in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_minf))
@@ -427,33 +427,33 @@
   val cfalse = cterm_of sg HOLogic.false_const
   val fm = norm_zero_one fm1
  in  case fm1 of 
-      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
+      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) => 
          if ((x=y) andalso (c1= zero) andalso (c2= one))
 	 then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_pinf))
          else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
 
-      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
+      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
   	if ((is_arith_rel fm) andalso (x = y) andalso (c1 = zero)  andalso (c2 = one)) 
 	then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf))
 	else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
 
-      |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+      |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) =>
         if ((y=x) andalso (c1 = zero)) then 
           if (pm1 = one) 
 	  then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_pinf)) 
 	  else (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf))
 	else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
   
-      |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+      |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => 
          if y=x then  let val cz = cterm_of sg (norm_zero_one z)
-			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero)
+			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero)
 	 	      in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_pinf)))
 		      end
 		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
-      |(Const("Divides.dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
+      |(Const("Divides.dvd",_)$ d $ (db as (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $
       c $ y ) $ z))) => 
          if y=x then  let val cz = cterm_of sg (norm_zero_one z)
-			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero)
+			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero)
 	 	      in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_pinf)))
 		      end
 		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
@@ -468,22 +468,22 @@
   let
 					val fm = norm_zero_one fm1
     in  case fm1 of 
-      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
+      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) => 
          if  (x=y) andalso (c1=zero) andalso (c2=one) 
 	   then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (neq_eq_pinf))
            else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
 
-      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
+      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
   	   if (is_arith_rel fm) andalso (x=y) andalso ((c1=zero) orelse (c1 = norm_zero_one zero)) andalso ((c2=one) orelse (c1 = norm_zero_one one))
 	     then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_pinf))
 	     else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf)) 
 
-      |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+      |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) =>
            if (y=x) andalso (c1 =zero) then 
             if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_pinf)) else
 	     (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_pinf))
 	    else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
-      |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+      |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => 
          if y=x then  let val cd = cterm_of sg (norm_zero_one d)
 	 		  val cz = cterm_of sg (norm_zero_one z)
 	 	      in(instantiate' [] [SOME cd,  SOME cz] (not_dvd_eq_pinf)) 
@@ -491,7 +491,7 @@
 
 		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
 		
-      |(Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+      |(Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => 
          if y=x then  let val cd = cterm_of sg (norm_zero_one d)
 	 		  val cz = cterm_of sg (norm_zero_one z)
 	 	      in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_pinf))
@@ -563,50 +563,52 @@
     val cat = cterm_of sg (norm_zero_one at)
   in
   case at of 
-   (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
+   (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) => 
       if  (x=y) andalso (c1=zero) andalso (c2=one) 
 	 then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B)
-	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one  z)))
-		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
+	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $(norm_zero_one  z)))
+        val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero ,dlcm))
 	 in  (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_bst_p_ne)))
 	 end
          else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
 
-   |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", T) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
+   |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, T) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
      if (is_arith_rel at) andalso (x=y)
-	then let val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_number 1)))
-	         in let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ bst_z $ B)
-	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const("HOL.minus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("HOL.one",HOLogic.intT))))
-		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
+    then let
+      val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_number 1)))
+    in
+      let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ bst_z $ B)
+	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const(@{const_name HOL.minus},T) $ (Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $ norm_zero_one z) $ HOLogic.mk_number HOLogic.intT 1))
+		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm))
 	 in  (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_bst_p_eq)))
 	 end
        end
          else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
 
-   |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+   |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) =>
         if (y=x) andalso (c1 =zero) then 
         if pm1 = one then 
 	  let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B)
-              val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
+              val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
 	  in  (instantiate' [] [SOME cfma,  SOME cdlcm]([th1,th2] MRS (not_bst_p_gt)))
 	    end
-	 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
+	 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm))
 	      in (instantiate' [] [SOME cfma, SOME cB,SOME (cterm_of sg (norm_zero_one z))] (th1 RS (not_bst_p_lt)))
 	      end
       else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
 
-   |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+   |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => 
       if y=x then  
            let val cz = cterm_of sg (norm_zero_one z)
-	       val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
+	       val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
  	     in (instantiate' []  [SOME cfma, SOME cB,SOME cz] (th1 RS (not_bst_p_ndvd)))
 	     end
       else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
 
-   |(Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+   |(Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => 
        if y=x then  
 	 let val cz = cterm_of sg (norm_zero_one z)
-	     val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
+	     val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
  	    in (instantiate' []  [SOME cfma,SOME cB,SOME cz] (th1 RS (not_bst_p_dvd)))
 	  end
       else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
@@ -654,49 +656,49 @@
     val cat = cterm_of sg (norm_zero_one at)
   in
   case at of 
-   (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
+   (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) => 
       if  (x=y) andalso (c1=zero) andalso (c2=one) 
 	 then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ A)
-	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one  z)))
-		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
+	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $(norm_zero_one  z)))
+		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm))
 	 in  (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_ast_p_ne)))
 	 end
          else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
 
-   |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", T) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
+   |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, T) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
      if (is_arith_rel at) andalso (x=y)
 	then let val ast_z = norm_zero_one (linear_sub [] one z )
 	         val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ ast_z $ A)
-	         val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (ast_z,Const("HOL.plus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("HOL.one",HOLogic.intT))))
-		 val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
+	         val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (ast_z,Const(@{const_name HOL.plus},T) $ (Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ one))
+		 val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm))
 	 in  (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_ast_p_eq)))
        end
          else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
 
-   |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+   |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) =>
         if (y=x) andalso (c1 =zero) then 
         if pm1 = (mk_number ~1) then 
 	  let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one z) $ A)
-              val th2 =  prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (zero,dlcm))
+              val th2 =  prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero,dlcm))
 	  in  (instantiate' [] [SOME cfma]([th2,th1] MRS (not_ast_p_lt)))
 	    end
-	 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
+	 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm))
 	      in (instantiate' [] [SOME cfma, SOME cA,SOME (cterm_of sg (norm_zero_one z))] (th1 RS (not_ast_p_gt)))
 	      end
       else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
 
-   |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+   |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => 
       if y=x then  
            let val cz = cterm_of sg (norm_zero_one z)
-	       val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
+	       val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
  	     in (instantiate' []  [SOME cfma, SOME cA,SOME cz] (th1 RS (not_ast_p_ndvd)))
 	     end
       else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
 
-   |(Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+   |(Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => 
        if y=x then  
 	 let val cz = cterm_of sg (norm_zero_one z)
-	     val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
+	     val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
  	    in (instantiate' []  [SOME cfma,SOME cA,SOME cz] (th1 RS (not_ast_p_dvd)))
 	  end
       else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
@@ -773,7 +775,7 @@
    |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI)
    |(Const("Not",_)$p) => ([p],fn [th] => th RS qe_Not)
    |(Const("Divides.dvd",_)$d$r) => 
-     if is_numeral d then ([], fn [] => (prove_elementar sg "lf" (HOLogic.mk_eq (r, lint vars r))) RS (instantiate' [] [NONE , NONE, SOME (cterm_of sg d)](linearize_dvd)))
+     if is_number d then ([], fn [] => (prove_elementar sg "lf" (HOLogic.mk_eq (r, lint vars r))) RS (instantiate' [] [NONE , NONE, SOME (cterm_of sg d)](linearize_dvd)))
      else (warning "Nonlinear Term --- Non numeral leftside at dvd";
        raise COOPER)
    |_ => ([], fn [] => prove_elementar sg "lf" (HOLogic.mk_eq (t, linform vars t)));
@@ -786,7 +788,7 @@
 fun coopermi_proof_of sg (x as Free(xn,xT)) fm B dlcm =
   (* Get the Bset thm*)
   let val (minf_eqth, minf_moddth) = minf_proof_of_c sg x dlcm fm 
-      val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (zero,dlcm));
+      val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero,dlcm));
       val nbstpthm = not_bst_p_proof_of_c sg x fm dlcm B fm
   in (dpos,minf_eqth,nbstpthm,minf_moddth)
 end;
@@ -796,7 +798,7 @@
 (* ------------------------------------------------------------------------- *)
 fun cooperpi_proof_of sg (x as Free(xn,xT)) fm A dlcm =
   let val (pinf_eqth,pinf_moddth) = pinf_proof_of_c sg x dlcm fm
-      val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (zero,dlcm));
+      val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero,dlcm));
       val nastpthm = not_ast_p_proof_of_c sg x fm dlcm A fm
   in (dpos,pinf_eqth,nastpthm,pinf_moddth)
 end;
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Integ/int_arith1.ML
--- a/src/HOL/Integ/int_arith1.ML	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Integ/int_arith1.ML	Thu May 17 19:49:40 2007 +0200
@@ -103,7 +103,7 @@
   fun prep_simproc (name, pats, proc) =
     Simplifier.simproc (the_context()) name pats proc;
 
-  fun is_numeral (Const("Numeral.number_of", _) $ w) = true
+  fun is_numeral (Const(@{const_name Numeral.number_of}, _) $ w) = true
     | is_numeral _ = false
 
   fun simplify_meta_eq f_number_of_eq f_eq =
@@ -118,13 +118,13 @@
     0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
   fun reorient_proc sg _ (_ $ t $ u) =
     case u of
-	Const("HOL.zero", _) => NONE
-      | Const("HOL.one", _) => NONE
-      | Const("Numeral.number_of", _) $ _ => NONE
+	Const(@{const_name HOL.zero}, _) => NONE
+      | Const(@{const_name HOL.one}, _) => NONE
+      | Const(@{const_name Numeral.number_of}, _) $ _ => NONE
       | _ => SOME (case t of
-		  Const("HOL.zero", _) => meta_zero_reorient
-		| Const("HOL.one", _) => meta_one_reorient
-		| Const("Numeral.number_of", _) $ _ => meta_number_of_reorient)
+		  Const(@{const_name HOL.zero}, _) => meta_zero_reorient
+		| Const(@{const_name HOL.one}, _) => meta_one_reorient
+		| Const(@{const_name Numeral.number_of}, _) $ _ => meta_number_of_reorient)
 
   val reorient_simproc = 
       prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc)
@@ -158,10 +158,10 @@
 fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) =
       (case numterm_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
   | numterm_ord
-     (Const("Numeral.number_of", _) $ v, Const("Numeral.number_of", _) $ w) =
+     (Const(@{const_name Numeral.number_of}, _) $ v, Const(@{const_name Numeral.number_of}, _) $ w) =
      num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w)
-  | numterm_ord (Const("Numeral.number_of", _) $ _, _) = LESS
-  | numterm_ord (_, Const("Numeral.number_of", _) $ _) = GREATER
+  | numterm_ord (Const(@{const_name Numeral.number_of}, _) $ _, _) = LESS
+  | numterm_ord (_, Const(@{const_name Numeral.number_of}, _) $ _) = GREATER
   | numterm_ord (t, u) =
       (case int_ord (size_of_term t, size_of_term u) of
         EQUAL =>
@@ -187,11 +187,11 @@
          handle TERM _ => find_first_numeral (t::past) terms)
   | find_first_numeral past [] = raise TERM("find_first_numeral", []);
 
-val mk_plus = HOLogic.mk_binop "HOL.plus";
+val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
 
 fun mk_minus t = 
   let val T = Term.fastype_of t
-  in Const ("HOL.uminus", T --> T) $ t
+  in Const (@{const_name HOL.uminus}, T --> T) $ t
   end;
 
 (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
@@ -203,22 +203,22 @@
 fun long_mk_sum T []        = mk_number T 0
   | long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
 
-val dest_plus = HOLogic.dest_bin "HOL.plus" Term.dummyT;
+val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} Term.dummyT;
 
 (*decompose additions AND subtractions as a sum*)
-fun dest_summing (pos, Const ("HOL.plus", _) $ t $ u, ts) =
+fun dest_summing (pos, Const (@{const_name HOL.plus}, _) $ t $ u, ts) =
         dest_summing (pos, t, dest_summing (pos, u, ts))
-  | dest_summing (pos, Const ("HOL.minus", _) $ t $ u, ts) =
+  | dest_summing (pos, Const (@{const_name HOL.minus}, _) $ t $ u, ts) =
         dest_summing (pos, t, dest_summing (not pos, u, ts))
   | dest_summing (pos, t, ts) =
         if pos then t::ts else mk_minus t :: ts;
 
 fun dest_sum t = dest_summing (true, t, []);
 
-val mk_diff = HOLogic.mk_binop "HOL.minus";
-val dest_diff = HOLogic.dest_bin "HOL.minus" Term.dummyT;
+val mk_diff = HOLogic.mk_binop @{const_name HOL.minus};
+val dest_diff = HOLogic.dest_bin @{const_name HOL.minus} Term.dummyT;
 
-val mk_times = HOLogic.mk_binop "HOL.times";
+val mk_times = HOLogic.mk_binop @{const_name HOL.times};
 
 fun mk_prod T = 
   let val one = mk_number T 1
@@ -231,7 +231,7 @@
 fun long_mk_prod T []        = mk_number T 1
   | long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts);
 
-val dest_times = HOLogic.dest_bin "HOL.times" Term.dummyT;
+val dest_times = HOLogic.dest_bin @{const_name HOL.times} Term.dummyT;
 
 fun dest_prod t =
       let val (t,u) = dest_times t
@@ -242,7 +242,7 @@
 fun mk_coeff (k, t) = mk_times (mk_number (Term.fastype_of t) k, t);
 
 (*Express t as a product of (possibly) a numeral with other sorted terms*)
-fun dest_coeff sign (Const ("HOL.uminus", _) $ t) = dest_coeff (~sign) t
+fun dest_coeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_coeff (~sign) t
   | dest_coeff sign t =
     let val ts = sort Term.term_ord (dest_prod t)
         val (n, ts') = find_first_numeral [] ts
@@ -338,8 +338,8 @@
 structure LessCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binrel "Orderings.less"
-  val dest_bal = HOLogic.dest_bin "Orderings.less" Term.dummyT
+  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
+  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
   val bal_add1 = less_add_iff1 RS trans
   val bal_add2 = less_add_iff2 RS trans
 );
@@ -347,8 +347,8 @@
 structure LeCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binrel "Orderings.less_eq"
-  val dest_bal = HOLogic.dest_bin "Orderings.less_eq" Term.dummyT
+  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
+  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
   val bal_add1 = le_add_iff1 RS trans
   val bal_add2 = le_add_iff2 RS trans
 );
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Integ/int_factor_simprocs.ML
--- a/src/HOL/Integ/int_factor_simprocs.ML	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Integ/int_factor_simprocs.ML	Thu May 17 19:49:40 2007 +0200
@@ -63,8 +63,8 @@
 structure DivCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binop "Divides.div"
-  val dest_bal = HOLogic.dest_bin "Divides.div" HOLogic.intT
+  val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
+  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT
   val cancel = int_mult_div_cancel1 RS trans
   val neg_exchanges = false
 )
@@ -73,8 +73,8 @@
 structure FieldDivCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binop "HOL.divide"
-  val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT
+  val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
   val cancel = @{thm mult_divide_cancel_left} RS trans
   val neg_exchanges = false
 )
@@ -102,8 +102,8 @@
 structure LessCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binrel "Orderings.less"
-  val dest_bal = HOLogic.dest_bin "Orderings.less" Term.dummyT
+  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
+  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
   val cancel = @{thm mult_less_cancel_left} RS trans
   val neg_exchanges = true
 )
@@ -111,8 +111,8 @@
 structure LeCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binrel "Orderings.less_eq"
-  val dest_bal = HOLogic.dest_bin "Orderings.less_eq" Term.dummyT
+  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
+  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
   val cancel = @{thm mult_le_cancel_left} RS trans
   val neg_exchanges = true
 )
@@ -270,8 +270,8 @@
 structure DivideCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binop "Divides.div"
-  val dest_bal = HOLogic.dest_bin "Divides.div" HOLogic.intT
+  val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
+  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT
   val simplify_meta_eq  = cancel_simplify_meta_eq int_mult_div_cancel_disj
 );
 
@@ -295,8 +295,8 @@
 structure FieldDivideCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binop "HOL.divide"
-  val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT
+  val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
   val simplify_meta_eq  = cancel_simplify_meta_eq @{thm mult_divide_cancel_eq_if}
 );
 
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Integ/nat_simprocs.ML
--- a/src/HOL/Integ/nat_simprocs.ML	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Integ/nat_simprocs.ML	Thu May 17 19:49:40 2007 +0200
@@ -6,10 +6,6 @@
 Simprocs for nat numerals.
 *)
 
-val Let_number_of = thm"Let_number_of";
-val Let_0 = thm"Let_0";
-val Let_1 = thm"Let_1";
-
 structure Nat_Numeral_Simprocs =
 struct
 
@@ -32,7 +28,7 @@
   | find_first_numeral past [] = raise TERM("find_first_numeral", []);
 
 val zero = mk_number 0;
-val mk_plus = HOLogic.mk_binop "HOL.plus";
+val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
 
 (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
 fun mk_sum []        = zero
@@ -43,7 +39,7 @@
 fun long_mk_sum []        = HOLogic.zero
   | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
 
-val dest_plus = HOLogic.dest_bin "HOL.plus" HOLogic.natT;
+val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
 
 
 (** Other simproc items **)
@@ -56,7 +52,7 @@
       diff_nat_number_of, le_number_of_eq_not_less,
       mult_nat_number_of, nat_number_of_mult_left, 
       less_nat_number_of, 
-      Let_number_of, nat_number_of] @
+      @{thm Let_number_of}, nat_number_of] @
      arith_simps @ rel_simps;
 
 fun prep_simproc (name, pats, proc) =
@@ -66,14 +62,14 @@
 (*** CancelNumerals simprocs ***)
 
 val one = mk_number 1;
-val mk_times = HOLogic.mk_binop "HOL.times";
+val mk_times = HOLogic.mk_binop @{const_name HOL.times};
 
 fun mk_prod [] = one
   | mk_prod [t] = t
   | mk_prod (t :: ts) = if t = one then mk_prod ts
                         else mk_times (t, mk_prod ts);
 
-val dest_times = HOLogic.dest_bin "HOL.times" HOLogic.natT;
+val dest_times = HOLogic.dest_bin @{const_name HOL.times} HOLogic.natT;
 
 fun dest_prod t =
       let val (t,u) = dest_times t
@@ -109,7 +105,7 @@
       handle TERM _ => (k, t::ts);
 
 (*Code for testing whether numerals are already used in the goal*)
-fun is_numeral (Const("Numeral.number_of", _) $ w) = true
+fun is_numeral (Const(@{const_name Numeral.number_of}, _) $ w) = true
   | is_numeral _ = false;
 
 fun prod_has_numeral t = exists is_numeral (dest_prod t);
@@ -130,7 +126,7 @@
 
 (*Simplify 1*n and n*1 to n*)
 val add_0s  = map rename_numerals [add_0, add_0_right];
-val mult_1s = map rename_numerals [thm"nat_mult_1", thm"nat_mult_1_right"];
+val mult_1s = map rename_numerals [@{thm nat_mult_1}, @{thm nat_mult_1_right}];
 
 (*Final simplification: cancel + and *; replace Numeral0 by 0 and Numeral1 by 1*)
 
@@ -185,8 +181,8 @@
 structure LessCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binrel "Orderings.less"
-  val dest_bal = HOLogic.dest_bin "Orderings.less" HOLogic.natT
+  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
+  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
   val bal_add1 = nat_less_add_iff1 RS trans
   val bal_add2 = nat_less_add_iff2 RS trans
 );
@@ -194,8 +190,8 @@
 structure LeCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binrel "Orderings.less_eq"
-  val dest_bal = HOLogic.dest_bin "Orderings.less_eq" HOLogic.natT
+  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
+  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
   val bal_add1 = nat_le_add_iff1 RS trans
   val bal_add2 = nat_le_add_iff2 RS trans
 );
@@ -203,8 +199,8 @@
 structure DiffCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binop "HOL.minus"
-  val dest_bal = HOLogic.dest_bin "HOL.minus" HOLogic.natT
+  val mk_bal   = HOLogic.mk_binop @{const_name HOL.minus}
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT
   val bal_add1 = nat_diff_add_eq1 RS trans
   val bal_add2 = nat_diff_add_eq2 RS trans
 );
@@ -287,8 +283,8 @@
 structure DivCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binop "Divides.div"
-  val dest_bal = HOLogic.dest_bin "Divides.div" HOLogic.natT
+  val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
+  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
   val cancel = nat_mult_div_cancel1 RS trans
   val neg_exchanges = false
 )
@@ -305,8 +301,8 @@
 structure LessCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binrel "Orderings.less"
-  val dest_bal = HOLogic.dest_bin "Orderings.less" HOLogic.natT
+  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
+  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
   val cancel = nat_mult_less_cancel1 RS trans
   val neg_exchanges = true
 )
@@ -314,8 +310,8 @@
 structure LeCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binrel "Orderings.less_eq"
-  val dest_bal = HOLogic.dest_bin "Orderings.less_eq" HOLogic.natT
+  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
+  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
   val cancel = nat_mult_le_cancel1 RS trans
   val neg_exchanges = true
 )
@@ -380,24 +376,24 @@
 structure LessCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binrel "Orderings.less"
-  val dest_bal = HOLogic.dest_bin "Orderings.less" HOLogic.natT
+  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
+  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
   val simplify_meta_eq  = cancel_simplify_meta_eq nat_mult_less_cancel_disj
 );
 
 structure LeCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binrel "Orderings.less_eq"
-  val dest_bal = HOLogic.dest_bin "Orderings.less_eq" HOLogic.natT
+  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
+  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
   val simplify_meta_eq  = cancel_simplify_meta_eq nat_mult_le_cancel_disj
 );
 
 structure DivideCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binop "Divides.div"
-  val dest_bal = HOLogic.dest_bin "Divides.div" HOLogic.natT
+  val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
+  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
   val simplify_meta_eq  = cancel_simplify_meta_eq nat_mult_div_cancel_disj
 );
 
@@ -527,7 +523,7 @@
 
 (* reduce contradictory <= to False *)
 val add_rules =
-  [thm "Let_number_of", Let_0, Let_1, nat_0, nat_1,
+  [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1}, nat_0, nat_1,
    add_nat_number_of, diff_nat_number_of, mult_nat_number_of,
    eq_nat_number_of, less_nat_number_of, le_number_of_eq_not_less,
    le_Suc_number_of,le_number_of_Suc,
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Integ/presburger.ML
--- a/src/HOL/Integ/presburger.ML	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Integ/presburger.ML	Thu May 17 19:49:40 2007 +0200
@@ -131,46 +131,46 @@
    ("op =", bT --> bT --> bT),
    ("Not", bT --> bT),
 
-   ("Orderings.less_eq", iT --> iT --> bT),
+   (@{const_name Orderings.less_eq}, iT --> iT --> bT),
    ("op =", iT --> iT --> bT),
-   ("Orderings.less", iT --> iT --> bT),
-   ("Divides.dvd", iT --> iT --> bT),
-   ("Divides.div", iT --> iT --> iT),
-   ("Divides.mod", iT --> iT --> iT),
-   ("HOL.plus", iT --> iT --> iT),
-   ("HOL.minus", iT --> iT --> iT),
-   ("HOL.times", iT --> iT --> iT),
-   ("HOL.abs", iT --> iT),
-   ("HOL.uminus", iT --> iT),
-   ("HOL.max", iT --> iT --> iT),
-   ("HOL.min", iT --> iT --> iT),
+   (@{const_name Orderings.less}, iT --> iT --> bT),
+   (@{const_name Divides.dvd}, iT --> iT --> bT),
+   (@{const_name Divides.div}, iT --> iT --> iT),
+   (@{const_name Divides.mod}, iT --> iT --> iT),
+   (@{const_name HOL.plus}, iT --> iT --> iT),
+   (@{const_name HOL.minus}, iT --> iT --> iT),
+   (@{const_name HOL.times}, iT --> iT --> iT),
+   (@{const_name HOL.abs}, iT --> iT),
+   (@{const_name HOL.uminus}, iT --> iT),
+   (@{const_name Orderings.max}, iT --> iT --> iT),
+   (@{const_name Orderings.min}, iT --> iT --> iT),
 
-   ("Orderings.less_eq", nT --> nT --> bT),
+   (@{const_name Orderings.less_eq}, nT --> nT --> bT),
    ("op =", nT --> nT --> bT),
-   ("Orderings.less", nT --> nT --> bT),
-   ("Divides.dvd", nT --> nT --> bT),
-   ("Divides.div", nT --> nT --> nT),
-   ("Divides.mod", nT --> nT --> nT),
-   ("HOL.plus", nT --> nT --> nT),
-   ("HOL.minus", nT --> nT --> nT),
-   ("HOL.times", nT --> nT --> nT),
-   ("Suc", nT --> nT),
-   ("HOL.max", nT --> nT --> nT),
-   ("HOL.min", nT --> nT --> nT),
+   (@{const_name Orderings.less}, nT --> nT --> bT),
+   (@{const_name Divides.dvd}, nT --> nT --> bT),
+   (@{const_name Divides.div}, nT --> nT --> nT),
+   (@{const_name Divides.mod}, nT --> nT --> nT),
+   (@{const_name HOL.plus}, nT --> nT --> nT),
+   (@{const_name HOL.minus}, nT --> nT --> nT),
+   (@{const_name HOL.times}, nT --> nT --> nT),
+   (@{const_name Suc}, nT --> nT),
+   (@{const_name Orderings.max}, nT --> nT --> nT),
+   (@{const_name Orderings.min}, nT --> nT --> nT),
 
-   ("Numeral.bit.B0", bitT),
-   ("Numeral.bit.B1", bitT),
-   ("Numeral.Bit", iT --> bitT --> iT),
-   ("Numeral.Pls", iT),
-   ("Numeral.Min", iT),
-   ("Numeral.number_of", iT --> iT),
-   ("Numeral.number_of", iT --> nT),
-   ("HOL.zero", nT),
-   ("HOL.zero", iT),
-   ("HOL.one", nT),
-   ("HOL.one", iT),
-   ("False", bT),
-   ("True", bT)];
+   (@{const_name Numeral.bit.B0}, bitT),
+   (@{const_name Numeral.bit.B1}, bitT),
+   (@{const_name Numeral.Bit}, iT --> bitT --> iT),
+   (@{const_name Numeral.Pls}, iT),
+   (@{const_name Numeral.Min}, iT),
+   (@{const_name Numeral.number_of}, iT --> iT),
+   (@{const_name Numeral.number_of}, iT --> nT),
+   (@{const_name HOL.zero}, nT),
+   (@{const_name HOL.zero}, iT),
+   (@{const_name HOL.one}, nT),
+   (@{const_name HOL.one}, iT),
+   (@{const_name False}, bT),
+   (@{const_name True}, bT)];
 
 (* Preparation of the formula to be sent to the Integer quantifier *)
 (* elimination procedure                                           *)
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Integ/reflected_cooper.ML
--- a/src/HOL/Integ/reflected_cooper.ML	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Integ/reflected_cooper.ML	Thu May 17 19:49:40 2007 +0200
@@ -8,29 +8,26 @@
 open Generated;
 (* pseudo reification : term -> intterm *)
 
-fun i_of_term vs t = 
-    case t of
-	Free(xn,xT) => (case AList.lookup (op =) vs t of 
-			   NONE   => error "Variable not found in the list!!"
-			 | SOME n => Var n)
-      | Const("HOL.zero",iT) => Cst 0
-      | Const("HOL.one",iT) => Cst 1
-      | Bound i => Var (nat (IntInf.fromInt i))
-      | Const("HOL.uminus",_)$t' => Neg (i_of_term vs t')
-      | Const ("HOL.plus",_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
-      | Const ("HOL.minus",_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
-      | Const ("HOL.times",_)$t1$t2 => Mult (i_of_term vs t1,i_of_term vs t2)
-      | Const ("Numeral.number_of",_)$t' => Cst (HOLogic.dest_numeral t')
-      | _ => error "i_of_term: unknown term";
-	
+fun i_of_term vs t =  case t of
+    Free(xn,xT) => (case AList.lookup (op =) vs t of 
+        NONE   => error "Variable not found in the list!!"
+      | SOME n => Var n)
+  | Const(@{const_name HOL.zero},iT) => Cst 0
+  | Const(@{const_name HOL.one},iT) => Cst 1
+  | Bound i => Var (nat (IntInf.fromInt i))
+  | Const(@{const_name HOL.uminus},_)$t' => Neg (i_of_term vs t')
+  | Const (@{const_name HOL.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
+  | Const (@{const_name HOL.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
+  | Const (@{const_name HOL.times},_)$t1$t2 => Mult (i_of_term vs t1,i_of_term vs t2)
+  | Const (@{const_name Numeral.number_of},_)$t' => Cst (HOLogic.dest_numeral t')
+  | _ => error "i_of_term: unknown term";
 
 (* pseudo reification : term -> QF *)
-fun qf_of_term vs t = 
-    case t of 
+fun qf_of_term vs t = case t of 
 	Const("True",_) => T
       | Const("False",_) => F
-      | Const("Orderings.less",_)$t1$t2 => Lt (i_of_term vs t1,i_of_term vs t2)
-      | Const("Orderings.less_eq",_)$t1$t2 => Le (i_of_term vs t1,i_of_term vs t2)
+      | Const(@{const_name Orderings.less},_)$t1$t2 => Lt (i_of_term vs t1,i_of_term vs t2)
+      | Const(@{const_name Orderings.less_eq},_)$t1$t2 => Le (i_of_term vs t1,i_of_term vs t2)
       | Const ("Divides.dvd",_)$t1$t2 => 
 	Divides(i_of_term vs t1,i_of_term vs t2)
       | Const("op =",eqT)$t1$t2 => 
@@ -77,25 +74,25 @@
     case t of 
 	Cst i => CooperDec.mk_number i
       | Var n => valOf (myassoc2 vs n)
-      | Neg t' => Const("HOL.uminus",iT --> iT)$(term_of_i vs t')
-      | Add(t1,t2) => Const("HOL.plus",[iT,iT] ---> iT)$
+      | Neg t' => Const(@{const_name HOL.uminus},iT --> iT)$(term_of_i vs t')
+      | Add(t1,t2) => Const(@{const_name HOL.plus},[iT,iT] ---> iT)$
 			   (term_of_i vs t1)$(term_of_i vs t2)
-      | Sub(t1,t2) => Const("HOL.minus",[iT,iT] ---> iT)$
+      | Sub(t1,t2) => Const(@{const_name HOL.minus},[iT,iT] ---> iT)$
 			   (term_of_i vs t1)$(term_of_i vs t2)
-      | Mult(t1,t2) => Const("HOL.times",[iT,iT] ---> iT)$
+      | Mult(t1,t2) => Const(@{const_name HOL.times},[iT,iT] ---> iT)$
 			   (term_of_i vs t1)$(term_of_i vs t2);
 
 fun term_of_qf vs t = 
     case t of 
 	T => HOLogic.true_const 
       | F => HOLogic.false_const
-      | Lt(t1,t2) => Const("Orderings.less",[iT,iT] ---> bT)$
+      | Lt(t1,t2) => Const(@{const_name Orderings.less},[iT,iT] ---> bT)$
 			   (term_of_i vs t1)$(term_of_i vs t2)
-      | Le(t1,t2) => Const("Orderings.less_eq",[iT,iT] ---> bT)$
+      | Le(t1,t2) => Const(@{const_name Orderings.less_eq},[iT,iT] ---> bT)$
 			  (term_of_i vs t1)$(term_of_i vs t2)
-      | Gt(t1,t2) => Const("Orderings.less",[iT,iT] ---> bT)$
+      | Gt(t1,t2) => Const(@{const_name Orderings.less},[iT,iT] ---> bT)$
 			   (term_of_i vs t2)$(term_of_i vs t1)
-      | Ge(t1,t2) => Const("Orderings.less_eq",[iT,iT] ---> bT)$
+      | Ge(t1,t2) => Const(@{const_name Orderings.less_eq},[iT,iT] ---> bT)$
 			  (term_of_i vs t2)$(term_of_i vs t1)
       | Eq(t1,t2) => Const("op =",[iT,iT] ---> bT)$
 			   (term_of_i vs t1)$(term_of_i vs t2)
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Library/Executable_Real.thy
--- a/src/HOL/Library/Executable_Real.thy	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Library/Executable_Real.thy	Thu May 17 19:49:40 2007 +0200
@@ -474,10 +474,11 @@
     val rT = HOLogic.realT;
 in if q = 1
   then HOLogic.mk_number rT p
-  else Const ("HOL.divide", rT --> rT --> rT) $
+  else @{term "op / \<Colon> real \<Rightarrow> real \<Rightarrow> real"} $
     HOLogic.mk_number rT p $ HOLogic.mk_number rT q
 end;
 *}
 
 consts_code INum ("")
+
 end
\ No newline at end of file
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Library/comm_ring.ML
--- a/src/HOL/Library/comm_ring.ML	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Library/comm_ring.ML	Thu May 17 19:49:40 2007 +0200
@@ -17,8 +17,8 @@
 exception CRing of string;
 
 (* Zero and One of the commutative ring *)
-fun cring_zero T = Const (@{const_name "HOL.zero"}, T);
-fun cring_one T = Const (@{const_name "HOL.one"}, T);
+fun cring_zero T = Const (@{const_name HOL.zero}, T);
+fun cring_one T = Const (@{const_name HOL.one}, T);
 
 (* reification functions *)
 (* add two polynom expressions *)
@@ -53,15 +53,15 @@
   | reif_pol T vs t = pol_Pc T $ t;
 
 (* reification of polynom expressions *)
-fun reif_polex T vs (Const (@{const_name "HOL.plus"}, _) $ a $ b) =
+fun reif_polex T vs (Const (@{const_name HOL.plus}, _) $ a $ b) =
       polex_add T $ reif_polex T vs a $ reif_polex T vs b
-  | reif_polex T vs (Const (@{const_name "HOL.minus"}, _) $ a $ b) =
+  | reif_polex T vs (Const (@{const_name HOL.minus}, _) $ a $ b) =
       polex_sub T $ reif_polex T vs a $ reif_polex T vs b
-  | reif_polex T vs (Const (@{const_name "HOL.times"}, _) $ a $ b) =
+  | reif_polex T vs (Const (@{const_name HOL.times}, _) $ a $ b) =
       polex_mul T $ reif_polex T vs a $ reif_polex T vs b
-  | reif_polex T vs (Const (@{const_name "HOL.uminus"}, _) $ a) =
+  | reif_polex T vs (Const (@{const_name HOL.uminus}, _) $ a) =
       polex_neg T $ reif_polex T vs a
-  | reif_polex T vs (Const (@{const_name "Nat.power"}, _) $ a $ n) =
+  | reif_polex T vs (Const (@{const_name Nat.power}, _) $ a $ n) =
       polex_pow T $ reif_polex T vs a $ n
   | reif_polex T vs t = polex_pol T $ reif_pol T vs t;
 
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Library/sct.ML
--- a/src/HOL/Library/sct.ML	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Library/sct.ML	Thu May 17 19:49:40 2007 +0200
@@ -63,8 +63,8 @@
     in Const (nth_const, lT --> HOLogic.natT --> T) $ xs end
 
 
-val less_nat_const = Const ("Orderings.less", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
-val lesseq_nat_const = Const ("Orderings.less_eq", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
+val less_nat_const = Const (@{const_name Orderings.less}, HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
+val lesseq_nat_const = Const (@{const_name Orderings.less_eq}, HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
 
 val has_edge_simps = [thm "Graphs.has_edge_def", thm "Graphs.dest_graph.simps"]
 
@@ -298,8 +298,7 @@
                                   THEN all_less_tac ts
 
 
-val length_const = "Nat.size"
-fun mk_length l = Const (length_const, fastype_of l --> HOLogic.natT) $ l
+fun mk_length l = HOLogic.size_const (fastype_of l) $ l;
 val length_simps = thms "SCT_Interpretation.length_simps"
 
 
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/OrderedGroup.thy	Thu May 17 19:49:40 2007 +0200
@@ -1058,7 +1058,8 @@
 (* term order for abelian groups *)
 
 fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a')
-      ["HOL.zero", "HOL.plus", "HOL.uminus", "HOL.minus"]
+      [@{const_name HOL.zero}, @{const_name HOL.plus},
+        @{const_name HOL.uminus}, @{const_name HOL.minus}]
   | agrp_ord _ = ~1;
 
 fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS);
@@ -1067,9 +1068,9 @@
   val ac1 = mk_meta_eq @{thm add_assoc};
   val ac2 = mk_meta_eq @{thm add_commute};
   val ac3 = mk_meta_eq @{thm add_left_commute};
-  fun solve_add_ac thy _ (_ $ (Const ("HOL.plus",_) $ _ $ _) $ _) =
+  fun solve_add_ac thy _ (_ $ (Const (@{const_name HOL.plus},_) $ _ $ _) $ _) =
         SOME ac1
-    | solve_add_ac thy _ (_ $ x $ (Const ("HOL.plus",_) $ y $ z)) =
+    | solve_add_ac thy _ (_ $ x $ (Const (@{const_name HOL.plus},_) $ y $ z)) =
         if termless_agrp (y, x) then SOME ac3 else NONE
     | solve_add_ac thy _ (_ $ x $ y) =
         if termless_agrp (y, x) then SOME ac2 else NONE
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Orderings.thy	Thu May 17 19:49:40 2007 +0200
@@ -380,11 +380,11 @@
           if of_sort t1
           then SOME (t1, "=", t2)
           else NONE
-      | dec (Const (@{const_name less_eq},  _) $ t1 $ t2) =
+      | dec (Const (@{const_name Orderings.less_eq},  _) $ t1 $ t2) =
           if of_sort t1
           then SOME (t1, "<=", t2)
           else NONE
-      | dec (Const (@{const_name less},  _) $ t1 $ t2) =
+      | dec (Const (@{const_name Orderings.less},  _) $ t1 $ t2) =
           if of_sort t1
           then SOME (t1, "<", t2)
           else NONE
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/ROOT.ML	Thu May 17 19:49:40 2007 +0200
@@ -26,14 +26,12 @@
 use "~~/src/Pure/General/rat.ML";
 use "~~/src/Provers/Arith/fast_lin_arith.ML";
 use "~~/src/Provers/Arith/cancel_sums.ML";
-use "~~/src/Provers/Arith/assoc_fold.ML";
 use "~~/src/Provers/quantifier1.ML";
 use "~~/src/Provers/project_rule.ML";
 use "~~/src/Provers/Arith/cancel_numerals.ML";
 use "~~/src/Provers/Arith/combine_numerals.ML";
 use "~~/src/Provers/Arith/cancel_numeral_factor.ML";
 use "~~/src/Provers/Arith/extract_common_term.ML";
-use "~~/src/Provers/Arith/cancel_div_mod.ML";
 use "~~/src/Provers/quasi.ML";
 use "~~/src/Provers/order.ML";
 
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Real/ferrante_rackoff_proof.ML
--- a/src/HOL/Real/ferrante_rackoff_proof.ML	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Real/ferrante_rackoff_proof.ML	Thu May 17 19:49:40 2007 +0200
@@ -24,10 +24,10 @@
     case fm of
         Const("op &",_)$p$q => (uset x p) union (uset x q)
       | Const("op |",_)$p$q => (uset x p) union (uset x q)
-      | Const("Orderings.less",_)$s$t => if s=x then [t] 
+      | Const(@{const_name Orderings.less},_)$s$t => if s=x then [t] 
                                else if t = x then [s]
                                else []
-      | Const("Orderings.less_eq",_)$s$t => if s=x then [t] 
+      | Const(@{const_name Orderings.less_eq},_)$s$t => if s=x then [t] 
                                else if t = x then [s]
                                else []
       | Const("op =",_)$s$t => if s=x then [t] 
@@ -96,7 +96,7 @@
             ([p,q],myfwd (minf_conj,pinf_conj, nmilbnd_conj, npiubnd_conj,lin_dense_conj))      
           | Const("op |",_)$p$q => 
             ([p,q],myfwd (minf_disj,pinf_disj, nmilbnd_disj,npiubnd_disj,lin_dense_disj))
-          | Const("Orderings.less",_)$s$t => 
+          | Const(@{const_name Orderings.less},_)$s$t => 
             if s= x then 
                 let val ct = cterm_of sg t
                     val tinU = nth uths (find_index (fn a => a=t) U)
@@ -127,7 +127,7 @@
                     val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
                 in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
                 end
-          | Const("Orderings.less_eq",_)$s$t => 
+          | Const(@{const_name Orderings.less_eq},_)$s$t => 
             if s= x then 
                 let val ct = cterm_of sg t
                     val tinU = nth uths (find_index (fn a => a=t) U)
@@ -287,8 +287,8 @@
 
 
     (* Normalization of arithmetical expressions *)
-val rzero = Const("HOL.zero",rT);
-val rone = Const("HOL.one",rT);
+val rzero = HOLogic.mk_number rT 0;
+val rone = HOLogic.mk_number rT 1;
 fun mk_real i = HOLogic.mk_number rT i;
 val dest_real = snd o HOLogic.dest_number;
 
@@ -301,18 +301,18 @@
 
 fun proveprod thy m n = 
     prove_bysimp thy (simpset_of thy) 
-                 (HOLogic.mk_eq(HOLogic.mk_binop "HOL.times" (mk_real m,mk_real n),mk_real (m*n)));
+                 (HOLogic.mk_eq(HOLogic.mk_binop @{const_name HOL.times} (mk_real m,mk_real n),mk_real (m*n)));
 fun proveadd thy m n = 
     prove_bysimp thy (simpset_of thy) 
-                 (HOLogic.mk_eq(HOLogic.mk_binop "HOL.plus" (mk_real m,mk_real n),mk_real (m+n)));
+                 (HOLogic.mk_eq(HOLogic.mk_binop @{const_name HOL.plus} (mk_real m,mk_real n),mk_real (m+n)));
 fun provediv thy m n = 
     let val g = gcd (m,n) 
         val m' = m div g
         val n'= n div g
     in
         (prove_bysimp thy (simpset_of thy) 
-                     (HOLogic.mk_eq(HOLogic.mk_binop "HOL.divide" (mk_real m,mk_real n),
-                                    HOLogic.mk_binop "HOL.divide" 
+                     (HOLogic.mk_eq(HOLogic.mk_binop @{const_name HOL.divide} (mk_real m,mk_real n),
+                                    HOLogic.mk_binop @{const_name HOL.divide} 
                                                      (mk_real m',mk_real n'))),m')
     end;
                  (* Multiplication of a normal term by a constant *)
@@ -321,7 +321,7 @@
 fun decomp_ncmulh thy c t = 
     if c = 0 then ([],fn _ => instantiate' [SOME crT] [SOME (cterm_of thy t)] @{thm mult_zero_left}) else 
     case t of 
-        Const("HOL.plus",_)$(Const("HOL.times",_)$c'$v)$b => 
+        Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c'$v)$b => 
         ([b],FWD (instantiate' [] [NONE, NONE, SOME (cterm_of thy v)] 
                                ((proveprod thy c (dest_real c')) RS ncmul_congh)))
       | _ => ([],fn _ => proveprod thy c (dest_real t));
@@ -353,8 +353,8 @@
 
 fun decomp_naddh thy vs (t,s) = 
     case (t,s) of 
-        (Const("HOL.plus",_)$(ctv as Const("HOL.times",_)$tc$tv)$tr, 
-         Const("HOL.plus",_)$(csv as Const("HOL.times",_)$sc$sv)$sr) =>
+        (Const(@{const_name HOL.plus},_)$(ctv as Const(@{const_name HOL.times},_)$tc$tv)$tr, 
+         Const(@{const_name HOL.plus},_)$(csv as Const(@{const_name HOL.times},_)$sc$sv)$sr) =>
         if tv = sv then 
             let val ntc = dest_real tc
                 val nsc = dest_real sc
@@ -368,9 +368,9 @@
         else if earlier vs tv sv 
         then ([(tr,s)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy ctv)] naddh_cong_ts))
         else ([(t,sr)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy csv)] naddh_cong_st))
-      | (Const("HOL.plus",_)$(ctv as Const("HOL.times",_)$tc$tv)$tr,_) => 
+      | (Const(@{const_name HOL.plus},_)$(ctv as Const(@{const_name HOL.times},_)$tc$tv)$tr,_) => 
         ([(tr,s)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy ctv)] naddh_cong_ts))
-      | (_,Const("HOL.plus",_)$(csv as Const("HOL.times",_)$sc$sv)$sr) => 
+      | (_,Const(@{const_name HOL.plus},_)$(csv as Const(@{const_name HOL.times},_)$sc$sv)$sr) => 
         ([(t,sr)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy csv)] naddh_cong_st))
       | (_,_) => ([], fn _ => proveadd thy (dest_real t) (dest_real s));
 
@@ -429,27 +429,27 @@
 fun decomp_normalizeh thy vs t =
     case t of
         Free _ => ([], fn _ => instantiate' [] [SOME(cterm_of thy t)] normalizeh_var)
-      | Const("HOL.uminus",_)$a => 
+      | Const(@{const_name HOL.uminus},_)$a => 
         ([a], 
          fn [tha] => let val _$(_$_$(_$a'$n')) = prop_of tha
                          in [tha,prove_nneg thy (a',dest_real n')] 
                                 MRS uminus_cong
                          end )
-      | Const("HOL.plus",_)$a$b => 
+      | Const(@{const_name HOL.plus},_)$a$b => 
         ([a,b], 
          fn [tha,thb] => let val _$(_$_$(_$a'$n')) = prop_of tha
                              val _$(_$_$(_$b'$m')) = prop_of thb
                          in [tha,thb,prove_nadd thy vs (a',dest_real n') (b',dest_real m')] 
                                 MRS plus_cong
                          end )
-      | Const("HOL.minus",_)$a$b => 
+      | Const(@{const_name HOL.minus},_)$a$b => 
         ([a,b], 
          fn [tha,thb] => let val _$(_$_$(_$a'$n')) = prop_of tha
                              val _$(_$_$(_$b'$m')) = prop_of thb
                          in [tha,thb,prove_nsub thy vs (a',dest_real n') (b',dest_real m')] 
                                 MRS diff_cong
                          end )
-      | Const("HOL.times",_)$a$b => 
+      | Const(@{const_name HOL.times},_)$a$b => 
         if can dest_real a 
         then ([b], fn [thb] => 
                       let val _$(_$_$(_$b'$m')) = prop_of thb
@@ -461,7 +461,7 @@
                       in [tha, prove_ncmul thy (dest_real b) (a',dest_real m')] MRS mult_cong2
                       end )
         else raise FAILURE "decomp_normalizeh: non linear term"
-      | Const("HOL.divide",_)$a$b => 
+      | Const(@{const_name HOL.divide},_)$a$b => 
         if can dest_real b
         then ([a], fn [tha] => 
                       let val _$(_$_$(_$a'$m')) = prop_of tha
@@ -473,7 +473,7 @@
 fun dest_xth vs th = 
     let val _$(_$_$(_$t$n)) = prop_of th
     in (case t of 
-            Const("HOL.plus",_)$(Const("HOL.times",_)$c$y)$r => 
+            Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$y)$r => 
             if vs = [] then (0,t,dest_real n)
             else if hd vs = y then (dest_real c, r,dest_real n)
             else (0,t,dest_real n)
@@ -482,12 +482,12 @@
 
 fun prove_strictsign thy n = 
     prove_bysimp thy (simpset_of thy) 
-                 (HOLogic.mk_binrel "Orderings.less" 
+                 (HOLogic.mk_binrel @{const_name Orderings.less} 
                                     (if n > 0 then (rzero, mk_real n) else (mk_real n, rzero))); 
 fun prove_fracsign thy (m,n) = 
-    let val mn = HOLogic.mk_binop "HOL.divide" (mk_real m, mk_real n)
+    let val mn = HOLogic.mk_binop @{const_name HOL.divide} (mk_real m, mk_real n)
     in prove_bysimp thy (simpset_of thy) 
-                 (HOLogic.mk_binrel "Orderings.less" 
+                 (HOLogic.mk_binrel @{const_name Orderings.less} 
                                     (if m*n > 0 then (rzero, mn) else (mn, rzero)))
     end; 
 
@@ -495,11 +495,11 @@
   | holbool_of false = HOLogic.false_const;
 
 fun prove_fracsign_eq thy s (m,n) = 
-    let fun f s = the (AList.lookup (op =) [("Orderings.less", op <),("Orderings.less_eq", op <=),("op =", op =)] s)
+    let fun f s = the (AList.lookup (op =) [(@{const_name Orderings.less}, op <),(@{const_name Orderings.less_eq}, op <=),("op =", op =)] s)
     in 
     prove_bysimp thy (simpset_of thy) (HOLogic.mk_eq
                  (HOLogic.mk_binrel s 
-                                    (HOLogic.mk_binop "HOL.divide" (mk_real m, mk_real n),rzero), 
+                                    (HOLogic.mk_binop @{const_name HOL.divide} (mk_real m, mk_real n),rzero), 
                                     holbool_of (f s (m*n,0))))
     end;
 
@@ -534,11 +534,11 @@
 
 fun prove_normalize thy vs at = 
     case at of 
-        Const("Orderings.less",_)$s$t => 
-        let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop "HOL.minus" (s,t))
+        Const(@{const_name Orderings.less},_)$s$t => 
+        let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop @{const_name HOL.minus} (s,t))
             val (cx,r,n) = dest_xth vs smtth
         in if cx = 0 then if can dest_real r 
-                          then [smtth, prove_fracsign_eq thy "Orderings.less" (dest_real r, n)]
+                          then [smtth, prove_fracsign_eq thy @{const_name Orderings.less} (dest_real r, n)]
                                    MRS normalize_ltground_cong
                           else [smtth, prove_strictsign thy n] 
                                    MRS (if n > 0 then normalize_ltnoxpos_cong 
@@ -554,11 +554,11 @@
                                         else normalize_ltxpos_cong)
                 end
         end
-      | Const("Orderings.less_eq",_)$s$t => 
-        let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop "HOL.minus" (s,t))
+      | Const(@{const_name Orderings.less_eq},_)$s$t => 
+        let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop @{const_name HOL.minus} (s,t))
             val (cx,r,n) = dest_xth vs smtth
         in if cx = 0 then if can dest_real r 
-                          then [smtth, prove_fracsign_eq thy "Orderings.less_eq" (dest_real r, n)]
+                          then [smtth, prove_fracsign_eq thy @{const_name Orderings.less_eq} (dest_real r, n)]
                                    MRS normalize_leground_cong
                           else [smtth, prove_strictsign thy n] 
                                    MRS (if n > 0 then normalize_lenoxpos_cong 
@@ -575,7 +575,7 @@
                 end
         end
       | Const("op =",_)$s$t => 
-        let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop "HOL.minus" (s,t))
+        let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop @{const_name HOL.minus} (s,t))
             val (cx,r,n) = dest_xth vs smtth
         in if cx = 0 then if can dest_real r 
                           then [smtth, provenz thy n, 
@@ -593,10 +593,10 @@
                                         else normalize_eqxpos_cong)
                 end
         end
-      | Const("Not",_)$(Const("Orderings.less",T)$s$t) => 
-        (prove_normalize thy vs (Const("Orderings.less_eq",T)$t$s)) RS normalize_not_lt
-      | Const("Not",_)$(Const("Orderings.less_eq",T)$s$t) => 
-        (prove_normalize thy vs (Const("Orderings.less",T)$t$s)) RS normalize_not_le
+      | Const("Not",_)$(Const(@{const_name Orderings.less},T)$s$t) => 
+        (prove_normalize thy vs (Const(@{const_name Orderings.less_eq},T)$t$s)) RS normalize_not_lt
+      | Const("Not",_)$(Const(@{const_name Orderings.less_eq},T)$s$t) => 
+        (prove_normalize thy vs (Const(@{const_name Orderings.less},T)$t$s)) RS normalize_not_le
       | (nt as Const("Not",_))$(Const("op =",T)$s$t) => 
         (prove_normalize thy vs (Const("op =",T)$s$t)) RS qe_Not
       | _ => instantiate' [SOME cbT] [SOME (cterm_of thy at)] refl;
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Tools/Presburger/cooper_dec.ML
--- a/src/HOL/Tools/Presburger/cooper_dec.ML	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Thu May 17 19:49:40 2007 +0200
@@ -10,12 +10,12 @@
 signature COOPER_DEC = 
 sig
   exception COOPER
-  val is_arith_rel : term -> bool
   val mk_number : IntInf.int -> term
-  val dest_number : term -> IntInf.int
-  val is_numeral : term -> bool
   val zero : term
   val one : term
+  val dest_number : term -> IntInf.int
+  val is_number : term -> bool
+  val is_arith_rel : term -> bool
   val linear_cmul : IntInf.int -> term -> term
   val linear_add : string list -> term -> term -> term 
   val linear_sub : string list -> term -> term -> term 
@@ -74,20 +74,13 @@
 (*Function is_arith_rel returns true if and only if the term is an operation of the 
 form [int,int]---> int*) 
  
-(*Transform a natural (FIXME?) number to a term*) 
-val mk_number = HOLogic.mk_number HOLogic.intT
- 
-(*Transform an Term to an natural (FIXME?) number*)
+val mk_number = HOLogic.mk_number HOLogic.intT;
+val zero = mk_number 0; 
+val one = mk_number 1; 
 fun dest_number t = let
     val (T, n) = HOLogic.dest_number t
   in if T = HOLogic.intT then n else error ("bad typ: " ^ Display.raw_string_of_typ T) end;
-
-(*Some terms often used for pattern matching*) 
-val zero = mk_number 0; 
-val one = mk_number 1; 
-
-(*Tests if a Term is representing a number*) 
-val is_numeral = can dest_number; 
+val is_number = can dest_number; 
 
 (*maps a unary natural function on a term containing an natural number*) 
 fun numeral1 f n = mk_number (f (dest_number n)); 
@@ -106,8 +99,8 @@
  
 fun linear_cmul n tm =  if n = 0 then zero else let fun times n k = n*k in  
   ( case tm of  
-     (Const("HOL.plus",T)  $  (Const ("HOL.times",T1 ) $c1 $  x1) $ rest) => 
-       Const("HOL.plus",T) $ ((Const("HOL.times",T1) $ (numeral1 (times n) c1) $ x1)) $ (linear_cmul n rest) 
+     (Const(@{const_name HOL.plus},T)  $  (Const (@{const_name HOL.times},T1 ) $c1 $  x1) $ rest) => 
+       Const(@{const_name HOL.plus},T) $ ((Const(@{const_name HOL.times},T1) $ (numeral1 (times n) c1) $ x1)) $ (linear_cmul n rest) 
     |_ =>  numeral1 (times n) tm) 
     end ; 
  
@@ -129,23 +122,23 @@
 fun linear_add vars tm1 tm2 = 
   let fun addwith x y = x + y in
  (case (tm1,tm2) of 
-	((Const ("HOL.plus",T1) $ ( Const("HOL.times",T2) $ c1 $  x1) $ rest1),(Const 
-	("HOL.plus",T3)$( Const("HOL.times",T4) $ c2 $  x2) $ rest2)) => 
+	((Const (@{const_name HOL.plus},T1) $ ( Const(@{const_name HOL.times},T2) $ c1 $  x1) $ rest1),(Const 
+	(@{const_name HOL.plus},T3)$( Const(@{const_name HOL.times},T4) $ c2 $  x2) $ rest2)) => 
          if x1 = x2 then 
               let val c = (numeral2 (addwith) c1 c2) 
 	      in 
               if c = zero then (linear_add vars rest1  rest2)  
-	      else (Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c $ x1) $ (linear_add vars  rest1 rest2)) 
+	      else (Const(@{const_name HOL.plus},T1) $ (Const(@{const_name HOL.times},T2) $ c $ x1) $ (linear_add vars  rest1 rest2)) 
               end 
 	   else 
-		if earlierv vars x1 x2 then (Const("HOL.plus",T1) $  
-		(Const("HOL.times",T2)$ c1 $ x1) $ (linear_add vars rest1 tm2)) 
-    	       else (Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c2 $ x2) $ (linear_add vars tm1 rest2)) 
-   	|((Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c1 $ x1) $ rest1) ,_) => 
-    	  (Const("HOL.plus",T1)$ (Const("HOL.times",T2) $ c1 $ x1) $ (linear_add vars 
+		if earlierv vars x1 x2 then (Const(@{const_name HOL.plus},T1) $  
+		(Const(@{const_name HOL.times},T2)$ c1 $ x1) $ (linear_add vars rest1 tm2)) 
+    	       else (Const(@{const_name HOL.plus},T1) $ (Const(@{const_name HOL.times},T2) $ c2 $ x2) $ (linear_add vars tm1 rest2)) 
+   	|((Const(@{const_name HOL.plus},T1) $ (Const(@{const_name HOL.times},T2) $ c1 $ x1) $ rest1) ,_) => 
+    	  (Const(@{const_name HOL.plus},T1)$ (Const(@{const_name HOL.times},T2) $ c1 $ x1) $ (linear_add vars 
 	  rest1 tm2)) 
-   	|(_, (Const("HOL.plus",T1) $(Const("HOL.times",T2) $ c2 $ x2) $ rest2)) => 
-      	  (Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c2 $ x2) $ (linear_add vars tm1 
+   	|(_, (Const(@{const_name HOL.plus},T1) $(Const(@{const_name HOL.times},T2) $ c2 $ x2) $ rest2)) => 
+      	  (Const(@{const_name HOL.plus},T1) $ (Const(@{const_name HOL.times},T2) $ c2 $ x2) $ (linear_add vars tm1 
 	  rest2)) 
    	| (_,_) => numeral2 (addwith) tm1 tm2) 
 	 
@@ -169,19 +162,19 @@
  c*Free(x,T) + t where c is a constant ant t is a Term which is not containing 
  Free(x,T)*) 
   
-fun lint vars tm = if is_numeral tm then tm else case tm of 
-   (Free (x,T)) =>  (HOLogic.mk_binop "HOL.plus" ((HOLogic.mk_binop "HOL.times" ((mk_number 1),Free (x,T))), zero)) 
-  |(Bound i) =>  (Const("HOL.plus",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ 
-  (Const("HOL.times",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_number 1) $ (Bound i)) $ zero) 
-  |(Const("HOL.uminus",_) $ t ) => (linear_neg (lint vars t)) 
-  |(Const("HOL.plus",_) $ s $ t) => (linear_add vars (lint vars s) (lint vars t)) 
-  |(Const("HOL.minus",_) $ s $ t) => (linear_sub vars (lint vars s) (lint vars t)) 
-  |(Const ("HOL.times",_) $ s $ t) => 
+fun lint vars tm = if is_number tm then tm else case tm of 
+   (Free (x,T)) =>  (HOLogic.mk_binop @{const_name HOL.plus} ((HOLogic.mk_binop @{const_name HOL.times} ((mk_number 1),Free (x,T))), zero)) 
+  |(Bound i) =>  (Const(@{const_name HOL.plus},HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ 
+  (Const(@{const_name HOL.times},HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_number 1) $ (Bound i)) $ zero) 
+  |(Const(@{const_name HOL.uminus},_) $ t ) => (linear_neg (lint vars t)) 
+  |(Const(@{const_name HOL.plus},_) $ s $ t) => (linear_add vars (lint vars s) (lint vars t)) 
+  |(Const(@{const_name HOL.minus},_) $ s $ t) => (linear_sub vars (lint vars s) (lint vars t)) 
+  |(Const (@{const_name HOL.times},_) $ s $ t) => 
         let val s' = lint vars s  
             val t' = lint vars t  
         in 
-        if is_numeral s' then (linear_cmul (dest_number s') t') 
-        else if is_numeral t' then (linear_cmul (dest_number t') s') 
+        if is_number s' then (linear_cmul (dest_number s') t') 
+        else if is_number t' then (linear_cmul (dest_number t') s') 
  
          else raise COOPER
          end 
@@ -196,20 +189,20 @@
 fun mkatom vars p t = Const(p,HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ zero $ (lint vars t); 
  
 fun linform vars (Const ("Divides.dvd",_) $ c $ t) =
-    if is_numeral c then   
+    if is_number c then   
       let val c' = (mk_number(abs(dest_number c)))  
       in (HOLogic.mk_binrel "Divides.dvd" (c,lint vars t)) 
       end 
     else (warning "Nonlinear term --- Non numeral leftside at dvd"
       ;raise COOPER)
-  |linform vars  (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ s $ t ) = (mkatom vars "op =" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s) ) 
-  |linform vars  (Const("Orderings.less",_)$ s $t ) = (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s))
-  |linform vars  (Const("op >",_) $ s $ t ) = (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t)) 
-  |linform vars  (Const("Orderings.less_eq",_)$ s $ t ) = 
-        (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_number 1)) $ s)) 
+  |linform vars  (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ s $ t ) = (mkatom vars "op =" (Const (@{const_name HOL.minus},HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s) ) 
+  |linform vars  (Const(@{const_name Orderings.less},_)$ s $t ) = (mkatom vars @{const_name Orderings.less} (Const (@{const_name HOL.minus},HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s))
+  |linform vars  (Const("op >",_) $ s $ t ) = (mkatom vars @{const_name Orderings.less} (Const (@{const_name HOL.minus},HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t)) 
+  |linform vars  (Const(@{const_name Orderings.less_eq},_)$ s $ t ) = 
+        (mkatom vars @{const_name Orderings.less} (Const (@{const_name HOL.minus},HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const(@{const_name HOL.plus},HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_number 1)) $ s)) 
   |linform vars  (Const("op >=",_)$ s $ t ) = 
-        (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> 
-	HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> 
+        (mkatom vars @{const_name Orderings.less} (Const (@{const_name HOL.minus},HOLogic.intT --> HOLogic.intT --> 
+	HOLogic.intT) $ (Const(@{const_name HOL.plus},HOLogic.intT --> HOLogic.intT --> 
 	HOLogic.intT) $s $(mk_number 1)) $ t)) 
  
    |linform vars  fm =  fm; 
@@ -219,8 +212,8 @@
 (* ------------------------------------------------------------------------- *) 
  
 fun posineq fm = case fm of  
- (Const ("Not",_)$(Const("Orderings.less",_)$ c $ t)) =>
-   (HOLogic.mk_binrel "Orderings.less"  (zero , (linear_sub [] (mk_number 1) (linear_add [] c t ) ))) 
+ (Const ("Not",_)$(Const(@{const_name Orderings.less},_)$ c $ t)) =>
+   (HOLogic.mk_binrel @{const_name Orderings.less}  (zero , (linear_sub [] (mk_number 1) (linear_add [] c t ) ))) 
   | ( Const ("op &",_) $ p $ q)  => HOLogic.mk_conj (posineq p,posineq q)
   | ( Const ("op |",_) $ p $ q ) => HOLogic.mk_disj (posineq p,posineq q)
   | _ => fm; 
@@ -236,7 +229,7 @@
 fun lcm_num a b = (abs a*b) div (gcd (abs a) (abs b)); 
  
 fun formlcm x fm = case fm of 
-    (Const (p,_)$ _ $(Const ("HOL.plus", _)$(Const ("HOL.times",_)$ c $ y ) $z ) ) =>  if 
+    (Const (p,_)$ _ $(Const (@{const_name HOL.plus}, _)$(Const (@{const_name HOL.times},_)$ c $ y ) $z ) ) =>  if 
     (is_arith_rel fm) andalso (x = y) then  (abs(dest_number c)) else 1 
   | ( Const ("Not", _) $p) => formlcm x p 
   | ( Const ("op &",_) $ p $ q) => lcm_num (formlcm x p) (formlcm x q) 
@@ -249,13 +242,13 @@
  
 fun adjustcoeff x l fm = 
      case fm of  
-      (Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $ 
+      (Const(p,_) $d $( Const (@{const_name HOL.plus}, _)$(Const (@{const_name HOL.times},_) $ 
       c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then  
         let val m = l div (dest_number c) 
-            val n = (if p = "Orderings.less" then abs(m) else m) 
-            val xtm = HOLogic.mk_binop "HOL.times" ((mk_number (m div n)), x) 
+            val n = (if p = @{const_name Orderings.less} then abs(m) else m) 
+            val xtm = HOLogic.mk_binop @{const_name HOL.times} ((mk_number (m div n)), x) 
 	in
-        (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) )))) 
+        (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop @{const_name HOL.plus} ( xtm ,( linear_cmul n z) )))) 
 	end 
 	else fm 
   |( Const ("Not", _) $ p) => HOLogic.Not $ (adjustcoeff x l p) 
@@ -272,8 +265,8 @@
       val fm' = adjustcoeff x l fm in
       if l = 1 then fm' 
 	 else 
-     let val xp = (HOLogic.mk_binop "HOL.plus"  
-     		((HOLogic.mk_binop "HOL.times" ((mk_number 1), x )), zero))
+     let val xp = (HOLogic.mk_binop @{const_name HOL.plus}  
+     		((HOLogic.mk_binop @{const_name HOL.times} ((mk_number 1), x )), zero))
 	in 
       HOLogic.conj $(HOLogic.mk_binrel "Divides.dvd" ((mk_number l) , xp )) $ (adjustcoeff x l fm) 
       end 
@@ -284,12 +277,12 @@
 (*
 fun adjustcoeffeq x l fm = 
     case fm of  
-      (Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $ 
+      (Const(p,_) $d $( Const (@{const_name HOL.plus}, _)$(Const (@{const_name HOL.times},_) $ 
       c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then  
         let val m = l div (dest_number c) 
-            val n = (if p = "Orderings.less" then abs(m) else m)  
-            val xtm = (HOLogic.mk_binop "HOL.times" ((mk_number ((m div n)*l) ), x))
-            in (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) )))) 
+            val n = (if p = @{const_name Orderings.less} then abs(m) else m)  
+            val xtm = (HOLogic.mk_binop @{const_name HOL.times} ((mk_number ((m div n)*l) ), x))
+            in (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop @{const_name HOL.plus} ( xtm ,( linear_cmul n z) )))) 
 	    end 
 	else fm 
   |( Const ("Not", _) $ p) => HOLogic.Not $ (adjustcoeffeq x l p) 
@@ -305,11 +298,11 @@
 (* ------------------------------------------------------------------------- *) 
  
 fun minusinf x fm = case fm of  
-    (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) => 
+    (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) => 
   	 if (is_arith_rel fm) andalso (x=y) andalso (c2 = one) andalso (c1 =zero) then HOLogic.false_const  
 	 				 else fm 
  
-  |(Const("Orderings.less",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z 
+  |(Const(@{const_name Orderings.less},_) $ c $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z 
   )) => if (x = y) 
 	then if (pm1 = one) andalso (c = zero) then HOLogic.false_const 
 	     else if (dest_number pm1 = ~1) andalso (c = zero) then HOLogic.true_const 
@@ -326,11 +319,11 @@
 (* ------------------------------------------------------------------------- *)
 
 fun plusinf x fm = case fm of
-    (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
+    (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
   	 if (is_arith_rel fm) andalso (x=y) andalso (c2 = one) andalso (c1 =zero) then HOLogic.false_const
 	 				 else fm
 
-  |(Const("Orderings.less",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z
+  |(Const(@{const_name Orderings.less},_) $ c $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z
   )) => if (x = y) 
 	then if (pm1 = one) andalso (c = zero) then HOLogic.true_const 
 	     else if (dest_number pm1 = ~1) andalso (c = zero) then HOLogic.false_const
@@ -346,7 +339,7 @@
 (* The LCM of all the divisors that involve x.                               *) 
 (* ------------------------------------------------------------------------- *) 
  
-fun divlcm x (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z ) ) =  
+fun divlcm x (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z ) ) =  
         if x = y then abs(dest_number d) else 1 
   |divlcm x ( Const ("Not", _) $ p) = divlcm x p 
   |divlcm x ( Const ("op &",_) $ p $ q) = lcm_num (divlcm x p) (divlcm x q) 
@@ -360,15 +353,15 @@
 fun bset x fm = case fm of 
    (Const ("Not", _) $ p) => if (is_arith_rel p) then  
           (case p of  
-	      (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $c2 $y) $a ) )  
+	      (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $c2 $y) $a ) )  
 	             => if (is_arith_rel p) andalso (x=	y) andalso (c2 = one) andalso (c1 = zero)  
 	                then [linear_neg a] 
 			else  bset x p 
    	  |_ =>[]) 
 			 
 			else bset x p 
-  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_number 1))]  else [] 
-  |(Const ("Orderings.less",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else [] 
+  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_number 1))]  else [] 
+  |(Const (@{const_name Orderings.less},_) $ c1$ (Const (@{const_name HOL.plus},_) $(Const (@{const_name HOL.times},_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else [] 
   |(Const ("op &",_) $ p $ q) => (bset x p) union (bset x q) 
   |(Const ("op |",_) $ p $ q) => (bset x p) union (bset x q) 
   |_ => []; 
@@ -380,15 +373,15 @@
 fun aset x fm = case fm of
    (Const ("Not", _) $ p) => if (is_arith_rel p) then
           (case p of
-	      (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $c2 $y) $a ) )
+	      (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $c2 $y) $a ) )
 	             => if (x=	y) andalso (c2 = one) andalso (c1 = zero)
 	                then [linear_neg a]
 			else  []
    	  |_ =>[])
 
 			else aset x p
-  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_number 1) a]  else []
-  |(Const ("Orderings.less",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_number (~1))) then [a] else []
+  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_number 1) a]  else []
+  |(Const (@{const_name Orderings.less},_) $ c1$ (Const (@{const_name HOL.plus},_) $(Const (@{const_name HOL.times},_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_number (~1))) then [a] else []
   |(Const ("op &",_) $ p $ q) => (aset x p) union (aset x q)
   |(Const ("op |",_) $ p $ q) => (aset x p) union (aset x q)
   |_ => [];
@@ -399,7 +392,7 @@
 (* ------------------------------------------------------------------------- *) 
  
 fun linrep vars x t fm = case fm of  
-   ((Const(p,_)$ d $ (Const("HOL.plus",_)$(Const("HOL.times",_)$ c $ y) $ z))) => 
+   ((Const(p,_)$ d $ (Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$ c $ y) $ z))) => 
       if (x = y) andalso (is_arith_rel fm)  
       then  
         let val ct = linear_cmul (dest_number c) t  
@@ -420,18 +413,18 @@
 exception DVD_UNKNOWN
 
 fun dvd_op (d, t) = 
- if not(is_numeral d) then raise DVD_UNKNOWN
+ if not(is_number d) then raise DVD_UNKNOWN
  else let 
    val dn = dest_number d
    fun coeffs_of x = case x of 
      Const(p,_) $ tl $ tr => 
-       if p = "HOL.plus" then (coeffs_of tl) union (coeffs_of tr)
-          else if p = "HOL.times" 
-	        then if (is_numeral tr) 
+       if p = @{const_name HOL.plus} then (coeffs_of tl) union (coeffs_of tr)
+          else if p = @{const_name HOL.times} 
+	        then if (is_number tr) 
 		 then [(dest_number tr) * (dest_number tl)] 
 		 else [dest_number tl]
 	        else []
-    |_ => if (is_numeral t) then [dest_number t]  else []
+    |_ => if (is_number t) then [dest_number t]  else []
    val ts = coeffs_of t
    in case ts of
      [] => raise DVD_UNKNOWN
@@ -440,7 +433,7 @@
 
 
 val operations = 
-  [("op =",op=), ("Orderings.less",IntInf.<), ("op >",IntInf.>), ("Orderings.less_eq",IntInf.<=) , 
+  [("op =",op=), (@{const_name Orderings.less},IntInf.<), ("op >",IntInf.>), (@{const_name Orderings.less_eq},IntInf.<=) , 
    ("op >=",IntInf.>=), 
    ("Divides.dvd",fn (x,y) =>((IntInf.mod(y, x)) = 0))]; 
  
@@ -648,8 +641,8 @@
     |mk_uni_vars T (Free (v,_)) = Free (v,T) 
     |mk_uni_vars T tm = tm; 
  
-fun mk_uni_int T (Const ("HOL.zero",T2)) = if T = T2 then (mk_number 0) else (Const ("HOL.zero",T2)) 
-    |mk_uni_int T (Const ("HOL.one",T2)) = if T = T2 then (mk_number 1) else (Const ("HOL.one",T2)) 
+fun mk_uni_int T (Const (@{const_name HOL.zero},T2)) = if T = T2 then (mk_number 0) else (Const (@{const_name HOL.zero},T2)) 
+    |mk_uni_int T (Const (@{const_name HOL.one},T2)) = if T = T2 then (mk_number 1) else (Const (@{const_name HOL.one},T2)) 
     |mk_uni_int T (node $ rest) = (mk_uni_int T node) $ (mk_uni_int T rest )  
     |mk_uni_int T (Abs(AV,AT,p)) = Abs(AV,AT,mk_uni_int T p) 
     |mk_uni_int T tm = tm; 
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Tools/Presburger/cooper_proof.ML
--- a/src/HOL/Tools/Presburger/cooper_proof.ML	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Tools/Presburger/cooper_proof.ML	Thu May 17 19:49:40 2007 +0200
@@ -155,17 +155,17 @@
 
 (* ------------------------------------------------------------------------- *)
 (*This function norm_zero_one  replaces the occurences of Numeral1 and Numeral0*)
-(*Respectively by their abstract representation Const("HOL.one",..) and Const("HOL.zero",..)*)
+(*Respectively by their abstract representation Const(@{const_name HOL.one},..) and Const(@{const_name HOL.zero},..)*)
 (*this is necessary because the theorems use this representation.*)
 (* This function should be elminated in next versions...*)
 (* ------------------------------------------------------------------------- *)
 
 fun norm_zero_one fm = case fm of
-  (Const ("HOL.times",_) $ c $ t) => 
+  (Const (@{const_name HOL.times},_) $ c $ t) => 
     if c = one then (norm_zero_one t)
     else if (dest_number c = ~1) 
-         then (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $ (norm_zero_one t))
-         else (HOLogic.mk_binop "HOL.times" (norm_zero_one c,norm_zero_one t))
+         then (Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $ (norm_zero_one t))
+         else (HOLogic.mk_binop @{const_name HOL.times} (norm_zero_one c,norm_zero_one t))
   |(node $ rest) => ((norm_zero_one node)$(norm_zero_one rest))
   |(Abs(x,T,p)) => (Abs(x,T,(norm_zero_one p)))
   |_ => fm;
@@ -251,32 +251,32 @@
 (*==================================================*)
 
 fun decomp_adjustcoeffeq sg x l fm = case fm of
-    (Const("Not",_)$(Const("Orderings.less",_) $(Const("HOL.zero",_)) $(rt as (Const ("HOL.plus", _)$(Const ("HOL.times",_) $    c $ y ) $z )))) => 
+    (Const("Not",_)$(Const(@{const_name Orderings.less},_) $ zero $(rt as (Const (@{const_name HOL.plus}, _)$(Const (@{const_name HOL.times},_) $    c $ y ) $z )))) => 
      let  
         val m = l div (dest_number c) 
         val n = if (x = y) then abs (m) else 1
-        val xtm = (HOLogic.mk_binop "HOL.times" ((mk_number ((m div n)*l) ), x)) 
+        val xtm = (HOLogic.mk_binop @{const_name HOL.times} ((mk_number ((m div n)*l) ), x)) 
         val rs = if (x = y) 
-                 then (HOLogic.mk_binrel "Orderings.less" (zero,linear_sub [] (mk_number n) (HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) )))) 
-                 else HOLogic.mk_binrel "Orderings.less" (zero,linear_sub [] one rt )
+                 then (HOLogic.mk_binrel @{const_name Orderings.less} (zero,linear_sub [] (mk_number n) (HOLogic.mk_binop @{const_name HOL.plus} ( xtm ,( linear_cmul n z) )))) 
+                 else HOLogic.mk_binrel @{const_name Orderings.less} (zero,linear_sub [] one rt )
         val ck = cterm_of sg (mk_number n)
         val cc = cterm_of sg c
         val ct = cterm_of sg z
         val cx = cterm_of sg y
         val pre = prove_elementar sg "lf" 
-            (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),(mk_number n)))
+            (HOLogic.mk_binrel @{const_name Orderings.less} (zero, mk_number n))
         val th1 = (pre RS (instantiate' [] [SOME ck,SOME cc, SOME cx, SOME ct] (ac_pi_eq)))
         in ([], fn [] => [th1,(prove_elementar sg "sa" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
         end
 
-  |(Const(p,_) $a $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $ 
+  |(Const(p,_) $a $( Const (@{const_name HOL.plus}, _)$(Const (@{const_name HOL.times},_) $ 
       c $ y ) $t )) => 
    if (is_arith_rel fm) andalso (x = y) 
    then  
         let val m = l div (dest_number c) 
-           val k = (if p = "Orderings.less" then abs(m) else m)  
-           val xtm = (HOLogic.mk_binop "HOL.times" ((mk_number ((m div k)*l) ), x))
-           val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul k t) )))) 
+           val k = (if p = @{const_name Orderings.less} then abs(m) else m)  
+           val xtm = (HOLogic.mk_binop @{const_name HOL.times} ((mk_number ((m div k)*l) ), x))
+           val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop @{const_name HOL.plus} ( xtm ,( linear_cmul k t) )))) 
 
            val ck = cterm_of sg (mk_number k)
            val cc = cterm_of sg c
@@ -286,23 +286,23 @@
 
 	   in 
 	case p of
-	  "Orderings.less" => 
+	  @{const_name Orderings.less} => 
 	let val pre = prove_elementar sg "lf" 
-	    (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),(mk_number k)))
+	    (HOLogic.mk_binrel @{const_name Orderings.less} (zero, mk_number k))
             val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct] (ac_lt_eq)))
 	in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
          end
 
            |"op =" =>
 	     let val pre = prove_elementar sg "lf" 
-	    (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_number k))))
+	    (HOLogic.Not $ (HOLogic.mk_binrel "op =" (zero, mk_number k)))
 	         val th1 = (pre RS(instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct] (ac_eq_eq)))
 	     in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
              end
 
              |"Divides.dvd" =>
 	       let val pre = prove_elementar sg "lf" 
-	   (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_number k))))
+	   (HOLogic.Not $ (HOLogic.mk_binrel "op =" (zero, mk_number k)))
                    val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct]) (ac_dvd_eq))
                in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
                         
@@ -331,31 +331,31 @@
    val cfalse = cterm_of sg HOLogic.false_const
    val fm = norm_zero_one fm1
   in  case fm1 of 
-      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
+      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) => 
          if (x=y) andalso (c1= zero) andalso (c2= one) then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf))
            else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
 
-      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
+      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
   	   if (is_arith_rel fm) andalso (x=y) andalso (c1= zero) andalso (c2= one) 
 	   then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf))
 	 	 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf)) 
 
-      |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+      |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) =>
            if (y=x) andalso (c1 = zero) then 
             if (pm1 = one) then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf)) else
 	     (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf))
 	    else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
   
-      |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+      |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => 
          if y=x then  let val cz = cterm_of sg (norm_zero_one z)
-			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero)
+			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero)
 	 	      in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_minf)))
 		      end
 		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
-      |(Const("Divides.dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
+      |(Const("Divides.dvd",_)$ d $ (db as (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $
       c $ y ) $ z))) => 
          if y=x then  let val cz = cterm_of sg (norm_zero_one z)
-			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero)
+			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero)
 	 	      in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_minf)))
 		      end
 		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
@@ -369,22 +369,22 @@
    let
    val fm = norm_zero_one fm1
     in  case fm1 of 
-      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
+      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) => 
          if  (x=y) andalso (c1=zero) andalso (c2=one) 
 	   then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (neq_eq_minf))
            else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
 
-      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
+      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
   	   if (is_arith_rel fm) andalso (x=y) andalso ((c1=zero) orelse (c1 = norm_zero_one zero)) andalso ((c2=one) orelse (c1 = norm_zero_one one))
 	     then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_minf))
 	     else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf)) 
 
-      |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+      |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) =>
            if (y=x) andalso (c1 =zero) then 
             if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_minf)) else
 	     (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_minf))
 	    else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
-      |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+      |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => 
          if y=x then  let val cd = cterm_of sg (norm_zero_one d)
 	 		  val cz = cterm_of sg (norm_zero_one z)
 	 	      in(instantiate' [] [SOME cd,  SOME cz] (not_dvd_eq_minf)) 
@@ -392,7 +392,7 @@
 
 		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
 		
-      |(Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+      |(Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => 
          if y=x then  let val cd = cterm_of sg (norm_zero_one d)
 	 		  val cz = cterm_of sg (norm_zero_one z)
 	 	      in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_minf))
@@ -427,33 +427,33 @@
   val cfalse = cterm_of sg HOLogic.false_const
   val fm = norm_zero_one fm1
  in  case fm1 of 
-      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
+      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) => 
          if ((x=y) andalso (c1= zero) andalso (c2= one))
 	 then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_pinf))
          else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
 
-      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
+      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
   	if ((is_arith_rel fm) andalso (x = y) andalso (c1 = zero)  andalso (c2 = one)) 
 	then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf))
 	else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
 
-      |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+      |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) =>
         if ((y=x) andalso (c1 = zero)) then 
           if (pm1 = one) 
 	  then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_pinf)) 
 	  else (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf))
 	else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
   
-      |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+      |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => 
          if y=x then  let val cz = cterm_of sg (norm_zero_one z)
-			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero)
+			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero)
 	 	      in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_pinf)))
 		      end
 		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
-      |(Const("Divides.dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
+      |(Const("Divides.dvd",_)$ d $ (db as (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $
       c $ y ) $ z))) => 
          if y=x then  let val cz = cterm_of sg (norm_zero_one z)
-			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero)
+			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero)
 	 	      in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_pinf)))
 		      end
 		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
@@ -468,22 +468,22 @@
   let
 					val fm = norm_zero_one fm1
     in  case fm1 of 
-      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
+      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) => 
          if  (x=y) andalso (c1=zero) andalso (c2=one) 
 	   then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (neq_eq_pinf))
            else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
 
-      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
+      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
   	   if (is_arith_rel fm) andalso (x=y) andalso ((c1=zero) orelse (c1 = norm_zero_one zero)) andalso ((c2=one) orelse (c1 = norm_zero_one one))
 	     then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_pinf))
 	     else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf)) 
 
-      |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+      |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) =>
            if (y=x) andalso (c1 =zero) then 
             if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_pinf)) else
 	     (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_pinf))
 	    else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
-      |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+      |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => 
          if y=x then  let val cd = cterm_of sg (norm_zero_one d)
 	 		  val cz = cterm_of sg (norm_zero_one z)
 	 	      in(instantiate' [] [SOME cd,  SOME cz] (not_dvd_eq_pinf)) 
@@ -491,7 +491,7 @@
 
 		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
 		
-      |(Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+      |(Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => 
          if y=x then  let val cd = cterm_of sg (norm_zero_one d)
 	 		  val cz = cterm_of sg (norm_zero_one z)
 	 	      in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_pinf))
@@ -563,50 +563,52 @@
     val cat = cterm_of sg (norm_zero_one at)
   in
   case at of 
-   (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
+   (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) => 
       if  (x=y) andalso (c1=zero) andalso (c2=one) 
 	 then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B)
-	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one  z)))
-		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
+	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $(norm_zero_one  z)))
+        val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero ,dlcm))
 	 in  (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_bst_p_ne)))
 	 end
          else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
 
-   |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", T) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
+   |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, T) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
      if (is_arith_rel at) andalso (x=y)
-	then let val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_number 1)))
-	         in let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ bst_z $ B)
-	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const("HOL.minus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("HOL.one",HOLogic.intT))))
-		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
+    then let
+      val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_number 1)))
+    in
+      let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ bst_z $ B)
+	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const(@{const_name HOL.minus},T) $ (Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $ norm_zero_one z) $ HOLogic.mk_number HOLogic.intT 1))
+		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm))
 	 in  (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_bst_p_eq)))
 	 end
        end
          else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
 
-   |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+   |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) =>
         if (y=x) andalso (c1 =zero) then 
         if pm1 = one then 
 	  let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B)
-              val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
+              val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
 	  in  (instantiate' [] [SOME cfma,  SOME cdlcm]([th1,th2] MRS (not_bst_p_gt)))
 	    end
-	 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
+	 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm))
 	      in (instantiate' [] [SOME cfma, SOME cB,SOME (cterm_of sg (norm_zero_one z))] (th1 RS (not_bst_p_lt)))
 	      end
       else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
 
-   |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+   |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => 
       if y=x then  
            let val cz = cterm_of sg (norm_zero_one z)
-	       val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
+	       val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
  	     in (instantiate' []  [SOME cfma, SOME cB,SOME cz] (th1 RS (not_bst_p_ndvd)))
 	     end
       else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
 
-   |(Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+   |(Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => 
        if y=x then  
 	 let val cz = cterm_of sg (norm_zero_one z)
-	     val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
+	     val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
  	    in (instantiate' []  [SOME cfma,SOME cB,SOME cz] (th1 RS (not_bst_p_dvd)))
 	  end
       else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
@@ -654,49 +656,49 @@
     val cat = cterm_of sg (norm_zero_one at)
   in
   case at of 
-   (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
+   (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) => 
       if  (x=y) andalso (c1=zero) andalso (c2=one) 
 	 then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ A)
-	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one  z)))
-		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
+	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $(norm_zero_one  z)))
+		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm))
 	 in  (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_ast_p_ne)))
 	 end
          else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
 
-   |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", T) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
+   |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, T) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
      if (is_arith_rel at) andalso (x=y)
 	then let val ast_z = norm_zero_one (linear_sub [] one z )
 	         val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ ast_z $ A)
-	         val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (ast_z,Const("HOL.plus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("HOL.one",HOLogic.intT))))
-		 val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
+	         val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (ast_z,Const(@{const_name HOL.plus},T) $ (Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ one))
+		 val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm))
 	 in  (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_ast_p_eq)))
        end
          else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
 
-   |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+   |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) =>
         if (y=x) andalso (c1 =zero) then 
         if pm1 = (mk_number ~1) then 
 	  let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one z) $ A)
-              val th2 =  prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (zero,dlcm))
+              val th2 =  prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero,dlcm))
 	  in  (instantiate' [] [SOME cfma]([th2,th1] MRS (not_ast_p_lt)))
 	    end
-	 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
+	 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm))
 	      in (instantiate' [] [SOME cfma, SOME cA,SOME (cterm_of sg (norm_zero_one z))] (th1 RS (not_ast_p_gt)))
 	      end
       else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
 
-   |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+   |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => 
       if y=x then  
            let val cz = cterm_of sg (norm_zero_one z)
-	       val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
+	       val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
  	     in (instantiate' []  [SOME cfma, SOME cA,SOME cz] (th1 RS (not_ast_p_ndvd)))
 	     end
       else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
 
-   |(Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+   |(Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => 
        if y=x then  
 	 let val cz = cterm_of sg (norm_zero_one z)
-	     val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
+	     val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
  	    in (instantiate' []  [SOME cfma,SOME cA,SOME cz] (th1 RS (not_ast_p_dvd)))
 	  end
       else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
@@ -773,7 +775,7 @@
    |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI)
    |(Const("Not",_)$p) => ([p],fn [th] => th RS qe_Not)
    |(Const("Divides.dvd",_)$d$r) => 
-     if is_numeral d then ([], fn [] => (prove_elementar sg "lf" (HOLogic.mk_eq (r, lint vars r))) RS (instantiate' [] [NONE , NONE, SOME (cterm_of sg d)](linearize_dvd)))
+     if is_number d then ([], fn [] => (prove_elementar sg "lf" (HOLogic.mk_eq (r, lint vars r))) RS (instantiate' [] [NONE , NONE, SOME (cterm_of sg d)](linearize_dvd)))
      else (warning "Nonlinear Term --- Non numeral leftside at dvd";
        raise COOPER)
    |_ => ([], fn [] => prove_elementar sg "lf" (HOLogic.mk_eq (t, linform vars t)));
@@ -786,7 +788,7 @@
 fun coopermi_proof_of sg (x as Free(xn,xT)) fm B dlcm =
   (* Get the Bset thm*)
   let val (minf_eqth, minf_moddth) = minf_proof_of_c sg x dlcm fm 
-      val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (zero,dlcm));
+      val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero,dlcm));
       val nbstpthm = not_bst_p_proof_of_c sg x fm dlcm B fm
   in (dpos,minf_eqth,nbstpthm,minf_moddth)
 end;
@@ -796,7 +798,7 @@
 (* ------------------------------------------------------------------------- *)
 fun cooperpi_proof_of sg (x as Free(xn,xT)) fm A dlcm =
   let val (pinf_eqth,pinf_moddth) = pinf_proof_of_c sg x dlcm fm
-      val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (zero,dlcm));
+      val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero,dlcm));
       val nastpthm = not_ast_p_proof_of_c sg x fm dlcm A fm
   in (dpos,pinf_eqth,nastpthm,pinf_moddth)
 end;
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Tools/Presburger/presburger.ML
--- a/src/HOL/Tools/Presburger/presburger.ML	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Tools/Presburger/presburger.ML	Thu May 17 19:49:40 2007 +0200
@@ -131,46 +131,46 @@
    ("op =", bT --> bT --> bT),
    ("Not", bT --> bT),
 
-   ("Orderings.less_eq", iT --> iT --> bT),
+   (@{const_name Orderings.less_eq}, iT --> iT --> bT),
    ("op =", iT --> iT --> bT),
-   ("Orderings.less", iT --> iT --> bT),
-   ("Divides.dvd", iT --> iT --> bT),
-   ("Divides.div", iT --> iT --> iT),
-   ("Divides.mod", iT --> iT --> iT),
-   ("HOL.plus", iT --> iT --> iT),
-   ("HOL.minus", iT --> iT --> iT),
-   ("HOL.times", iT --> iT --> iT),
-   ("HOL.abs", iT --> iT),
-   ("HOL.uminus", iT --> iT),
-   ("HOL.max", iT --> iT --> iT),
-   ("HOL.min", iT --> iT --> iT),
+   (@{const_name Orderings.less}, iT --> iT --> bT),
+   (@{const_name Divides.dvd}, iT --> iT --> bT),
+   (@{const_name Divides.div}, iT --> iT --> iT),
+   (@{const_name Divides.mod}, iT --> iT --> iT),
+   (@{const_name HOL.plus}, iT --> iT --> iT),
+   (@{const_name HOL.minus}, iT --> iT --> iT),
+   (@{const_name HOL.times}, iT --> iT --> iT),
+   (@{const_name HOL.abs}, iT --> iT),
+   (@{const_name HOL.uminus}, iT --> iT),
+   (@{const_name Orderings.max}, iT --> iT --> iT),
+   (@{const_name Orderings.min}, iT --> iT --> iT),
 
-   ("Orderings.less_eq", nT --> nT --> bT),
+   (@{const_name Orderings.less_eq}, nT --> nT --> bT),
    ("op =", nT --> nT --> bT),
-   ("Orderings.less", nT --> nT --> bT),
-   ("Divides.dvd", nT --> nT --> bT),
-   ("Divides.div", nT --> nT --> nT),
-   ("Divides.mod", nT --> nT --> nT),
-   ("HOL.plus", nT --> nT --> nT),
-   ("HOL.minus", nT --> nT --> nT),
-   ("HOL.times", nT --> nT --> nT),
-   ("Suc", nT --> nT),
-   ("HOL.max", nT --> nT --> nT),
-   ("HOL.min", nT --> nT --> nT),
+   (@{const_name Orderings.less}, nT --> nT --> bT),
+   (@{const_name Divides.dvd}, nT --> nT --> bT),
+   (@{const_name Divides.div}, nT --> nT --> nT),
+   (@{const_name Divides.mod}, nT --> nT --> nT),
+   (@{const_name HOL.plus}, nT --> nT --> nT),
+   (@{const_name HOL.minus}, nT --> nT --> nT),
+   (@{const_name HOL.times}, nT --> nT --> nT),
+   (@{const_name Suc}, nT --> nT),
+   (@{const_name Orderings.max}, nT --> nT --> nT),
+   (@{const_name Orderings.min}, nT --> nT --> nT),
 
-   ("Numeral.bit.B0", bitT),
-   ("Numeral.bit.B1", bitT),
-   ("Numeral.Bit", iT --> bitT --> iT),
-   ("Numeral.Pls", iT),
-   ("Numeral.Min", iT),
-   ("Numeral.number_of", iT --> iT),
-   ("Numeral.number_of", iT --> nT),
-   ("HOL.zero", nT),
-   ("HOL.zero", iT),
-   ("HOL.one", nT),
-   ("HOL.one", iT),
-   ("False", bT),
-   ("True", bT)];
+   (@{const_name Numeral.bit.B0}, bitT),
+   (@{const_name Numeral.bit.B1}, bitT),
+   (@{const_name Numeral.Bit}, iT --> bitT --> iT),
+   (@{const_name Numeral.Pls}, iT),
+   (@{const_name Numeral.Min}, iT),
+   (@{const_name Numeral.number_of}, iT --> iT),
+   (@{const_name Numeral.number_of}, iT --> nT),
+   (@{const_name HOL.zero}, nT),
+   (@{const_name HOL.zero}, iT),
+   (@{const_name HOL.one}, nT),
+   (@{const_name HOL.one}, iT),
+   (@{const_name False}, bT),
+   (@{const_name True}, bT)];
 
 (* Preparation of the formula to be sent to the Integer quantifier *)
 (* elimination procedure                                           *)
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Tools/Presburger/reflected_cooper.ML
--- a/src/HOL/Tools/Presburger/reflected_cooper.ML	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Tools/Presburger/reflected_cooper.ML	Thu May 17 19:49:40 2007 +0200
@@ -8,29 +8,26 @@
 open Generated;
 (* pseudo reification : term -> intterm *)
 
-fun i_of_term vs t = 
-    case t of
-	Free(xn,xT) => (case AList.lookup (op =) vs t of 
-			   NONE   => error "Variable not found in the list!!"
-			 | SOME n => Var n)
-      | Const("HOL.zero",iT) => Cst 0
-      | Const("HOL.one",iT) => Cst 1
-      | Bound i => Var (nat (IntInf.fromInt i))
-      | Const("HOL.uminus",_)$t' => Neg (i_of_term vs t')
-      | Const ("HOL.plus",_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
-      | Const ("HOL.minus",_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
-      | Const ("HOL.times",_)$t1$t2 => Mult (i_of_term vs t1,i_of_term vs t2)
-      | Const ("Numeral.number_of",_)$t' => Cst (HOLogic.dest_numeral t')
-      | _ => error "i_of_term: unknown term";
-	
+fun i_of_term vs t =  case t of
+    Free(xn,xT) => (case AList.lookup (op =) vs t of 
+        NONE   => error "Variable not found in the list!!"
+      | SOME n => Var n)
+  | Const(@{const_name HOL.zero},iT) => Cst 0
+  | Const(@{const_name HOL.one},iT) => Cst 1
+  | Bound i => Var (nat (IntInf.fromInt i))
+  | Const(@{const_name HOL.uminus},_)$t' => Neg (i_of_term vs t')
+  | Const (@{const_name HOL.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
+  | Const (@{const_name HOL.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
+  | Const (@{const_name HOL.times},_)$t1$t2 => Mult (i_of_term vs t1,i_of_term vs t2)
+  | Const (@{const_name Numeral.number_of},_)$t' => Cst (HOLogic.dest_numeral t')
+  | _ => error "i_of_term: unknown term";
 
 (* pseudo reification : term -> QF *)
-fun qf_of_term vs t = 
-    case t of 
+fun qf_of_term vs t = case t of 
 	Const("True",_) => T
       | Const("False",_) => F
-      | Const("Orderings.less",_)$t1$t2 => Lt (i_of_term vs t1,i_of_term vs t2)
-      | Const("Orderings.less_eq",_)$t1$t2 => Le (i_of_term vs t1,i_of_term vs t2)
+      | Const(@{const_name Orderings.less},_)$t1$t2 => Lt (i_of_term vs t1,i_of_term vs t2)
+      | Const(@{const_name Orderings.less_eq},_)$t1$t2 => Le (i_of_term vs t1,i_of_term vs t2)
       | Const ("Divides.dvd",_)$t1$t2 => 
 	Divides(i_of_term vs t1,i_of_term vs t2)
       | Const("op =",eqT)$t1$t2 => 
@@ -77,25 +74,25 @@
     case t of 
 	Cst i => CooperDec.mk_number i
       | Var n => valOf (myassoc2 vs n)
-      | Neg t' => Const("HOL.uminus",iT --> iT)$(term_of_i vs t')
-      | Add(t1,t2) => Const("HOL.plus",[iT,iT] ---> iT)$
+      | Neg t' => Const(@{const_name HOL.uminus},iT --> iT)$(term_of_i vs t')
+      | Add(t1,t2) => Const(@{const_name HOL.plus},[iT,iT] ---> iT)$
 			   (term_of_i vs t1)$(term_of_i vs t2)
-      | Sub(t1,t2) => Const("HOL.minus",[iT,iT] ---> iT)$
+      | Sub(t1,t2) => Const(@{const_name HOL.minus},[iT,iT] ---> iT)$
 			   (term_of_i vs t1)$(term_of_i vs t2)
-      | Mult(t1,t2) => Const("HOL.times",[iT,iT] ---> iT)$
+      | Mult(t1,t2) => Const(@{const_name HOL.times},[iT,iT] ---> iT)$
 			   (term_of_i vs t1)$(term_of_i vs t2);
 
 fun term_of_qf vs t = 
     case t of 
 	T => HOLogic.true_const 
       | F => HOLogic.false_const
-      | Lt(t1,t2) => Const("Orderings.less",[iT,iT] ---> bT)$
+      | Lt(t1,t2) => Const(@{const_name Orderings.less},[iT,iT] ---> bT)$
 			   (term_of_i vs t1)$(term_of_i vs t2)
-      | Le(t1,t2) => Const("Orderings.less_eq",[iT,iT] ---> bT)$
+      | Le(t1,t2) => Const(@{const_name Orderings.less_eq},[iT,iT] ---> bT)$
 			  (term_of_i vs t1)$(term_of_i vs t2)
-      | Gt(t1,t2) => Const("Orderings.less",[iT,iT] ---> bT)$
+      | Gt(t1,t2) => Const(@{const_name Orderings.less},[iT,iT] ---> bT)$
 			   (term_of_i vs t2)$(term_of_i vs t1)
-      | Ge(t1,t2) => Const("Orderings.less_eq",[iT,iT] ---> bT)$
+      | Ge(t1,t2) => Const(@{const_name Orderings.less_eq},[iT,iT] ---> bT)$
 			  (term_of_i vs t2)$(term_of_i vs t1)
       | Eq(t1,t2) => Const("op =",[iT,iT] ---> bT)$
 			   (term_of_i vs t1)$(term_of_i vs t2)
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Tools/function_package/lexicographic_order.ML
--- a/src/HOL/Tools/function_package/lexicographic_order.ML	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Thu May 17 19:49:40 2007 +0200
@@ -62,7 +62,7 @@
     | _ => [(t, tt)]
            
 fun mk_base_fun_header fulltyp (t, typ) =
-    Abs ("x", fulltyp, Const("Nat.size", typ --> HOLogic.natT) $ t)
+    Abs ("x", fulltyp, HOLogic.size_const typ $ t)
          
 fun mk_base_funs (tt: typ) = 
     mk_base_fun_bodys (Bound 0) tt |>
@@ -121,13 +121,13 @@
 fun mk_cell (thy : theory) (vars, prems) (lhs, rhs) = 
     let 
       val goals = mk_goal (vars, prems, lhs, rhs) 
-      val less_thm = goals "Orderings.less" |> prove thy
+      val less_thm = goals "Orderings.ord_class.less" |> prove thy
     in
       if Thm.no_prems less_thm then
         Less (Goal.finish less_thm)
       else
         let
-          val lesseq_thm = goals "Orderings.less_eq" |> prove thy
+          val lesseq_thm = goals "Orderings.ord_class.less_eq" |> prove thy
         in
           if Thm.no_prems lesseq_thm then
             LessEq (Goal.finish lesseq_thm)
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Thu May 17 19:49:40 2007 +0200
@@ -158,7 +158,7 @@
     case concl of
       Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
     | _ $ (Const ("op =", _) $ _ $ _) => eq2mono thm
-    | _ $ (Const ("Orderings.less_eq", _) $ _ $ _) =>
+    | _ $ (Const ("Orderings.ord_class.less_eq", _) $ _ $ _) =>
       [dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
          (resolve_tac [le_funI, le_boolI'])) thm))]
     | _ => [thm]
@@ -532,7 +532,7 @@
          (make_bool_args HOLogic.mk_not I bs i)) preds));
 
     val ind_concl = HOLogic.mk_Trueprop
-      (HOLogic.mk_binrel "Orderings.less_eq" (rec_const, ind_pred));
+      (HOLogic.mk_binrel "Orderings.ord_class.less_eq" (rec_const, ind_pred));
 
     val raw_fp_induct = (mono RS (fp_def RS def_lfp_induct));
 
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Tools/numeral_syntax.ML
--- a/src/HOL/Tools/numeral_syntax.ML	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Tools/numeral_syntax.ML	Thu May 17 19:49:40 2007 +0200
@@ -20,16 +20,16 @@
 fun mk_bin num =
   let
     val {leading_zeros = z, value, ...} = Syntax.read_xnum num;
-    fun bit b bs = Syntax.const "\\<^const>Numeral.Bit" $ bs $ HOLogic.mk_bit b;
-    fun mk 0 = (* FIXME funpow z (bit 0) *) (Syntax.const "\\<^const>Numeral.Pls")
-      | mk ~1 = (* FIXME funpow z (bit 1) *) (Syntax.const "\\<^const>Numeral.Min")
+    fun bit b bs = Syntax.const @{const_name Numeral.Bit} $ bs $ HOLogic.mk_bit b;
+    fun mk 0 = (* FIXME funpow z (bit 0) *) (Syntax.const @{const_name Numeral.Pls})
+      | mk ~1 = (* FIXME funpow z (bit 1) *) (Syntax.const @{const_name Numeral.Min})
       | mk i = let val (q, r) = IntInf.divMod (i, 2) in bit (IntInf.toInt r) (mk q) end;
   in mk value end;
 
 in
 
 fun numeral_tr (*"_Numeral"*) [t as Const (num, _)] =
-      Syntax.const "Numeral.number_of" $ mk_bin num
+      Syntax.const @{const_name Numeral.number_of} $ mk_bin num
   | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
 
 end;
@@ -39,15 +39,15 @@
 
 local
 
-fun dest_bit (Const ("Numeral.bit.B0", _)) = 0
-  | dest_bit (Const ("Numeral.bit.B1", _)) = 1
+fun dest_bit (Const (@{const_syntax Numeral.bit.B0}, _)) = 0
+  | dest_bit (Const (@{const_syntax Numeral.bit.B1}, _)) = 1
   | dest_bit (Const ("bit.B0", _)) = 0
   | dest_bit (Const ("bit.B1", _)) = 1
   | dest_bit _ = raise Match;
 
-fun dest_bin (Const ("\\<^const>Numeral.Pls", _)) = []
-  | dest_bin (Const ("\\<^const>Numeral.Min", _)) = [~1]
-  | dest_bin (Const ("\\<^const>Numeral.Bit", _) $ bs $ b) = dest_bit b :: dest_bin bs
+fun dest_bin (Const (@{const_syntax "Numeral.Pls"}, _)) = []
+  | dest_bin (Const (@{const_syntax "Numeral.Min"}, _)) = [~1]
+  | dest_bin (Const (@{const_syntax "Numeral.Bit"}, _) $ bs $ b) = dest_bit b :: dest_bin bs
   | dest_bin _ = raise Match;
 
 fun leading _ [] = 0
@@ -89,6 +89,6 @@
 
 val setup =
   Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #>
-  Theory.add_trfunsT [("\\<^const>Numeral.number_of", numeral_tr')];
+  Theory.add_trfunsT [(@{const_syntax Numeral.number_of}, numeral_tr')];
 
 end;
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Tools/refute.ML	Thu May 17 19:49:40 2007 +0200
@@ -696,13 +696,13 @@
       | Const ("Finite_Set.card", _)    => t
       | Const ("Finite_Set.Finites", _) => t
       | Const ("Finite_Set.finite", _)  => t
-      | Const ("Orderings.less", Type ("fun", [Type ("nat", []),
+      | Const (@{const_name Orderings.less}, Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => t
-      | Const ("HOL.plus", Type ("fun", [Type ("nat", []),
+      | Const (@{const_name HOL.plus}, Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
-      | Const ("HOL.minus", Type ("fun", [Type ("nat", []),
+      | Const (@{const_name HOL.minus}, Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
-      | Const ("HOL.times", Type ("fun", [Type ("nat", []),
+      | Const (@{const_name HOL.times}, Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
       | Const ("List.op @", _)          => t
       | Const ("Lfp.lfp", _)            => t
@@ -883,16 +883,16 @@
       | Const ("Finite_Set.card", T)    => collect_type_axioms (axs, T)
       | Const ("Finite_Set.Finites", T) => collect_type_axioms (axs, T)
       | Const ("Finite_Set.finite", T)  => collect_type_axioms (axs, T)
-      | Const ("Orderings.less", T as Type ("fun", [Type ("nat", []),
+      | Const (@{const_name Orderings.less}, T as Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
           collect_type_axioms (axs, T)
-      | Const ("HOL.plus", T as Type ("fun", [Type ("nat", []),
+      | Const (@{const_name HOL.plus}, T as Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
           collect_type_axioms (axs, T)
-      | Const ("HOL.minus", T as Type ("fun", [Type ("nat", []),
+      | Const (@{const_name HOL.minus}, T as Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
           collect_type_axioms (axs, T)
-      | Const ("HOL.times", T as Type ("fun", [Type ("nat", []),
+      | Const (@{const_name HOL.times}, T as Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
           collect_type_axioms (axs, T)
       | Const ("List.op @", T)          => collect_type_axioms (axs, T)
@@ -2608,7 +2608,7 @@
 
   fun Nat_less_interpreter thy model args t =
     case t of
-      Const ("Orderings.less", Type ("fun", [Type ("nat", []),
+      Const (@{const_name Orderings.less}, Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
       let
         val (i_nat, _, _) = interpret thy model
@@ -2634,7 +2634,7 @@
 
   fun Nat_plus_interpreter thy model args t =
     case t of
-      Const ("HOL.plus", Type ("fun", [Type ("nat", []),
+      Const (@{const_name HOL.plus}, Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
       let
         val (i_nat, _, _) = interpret thy model
@@ -2668,7 +2668,7 @@
 
   fun Nat_minus_interpreter thy model args t =
     case t of
-      Const ("HOL.minus", Type ("fun", [Type ("nat", []),
+      Const (@{const_name HOL.minus}, Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
       let
         val (i_nat, _, _) = interpret thy model
@@ -2699,7 +2699,7 @@
 
   fun Nat_times_interpreter thy model args t =
     case t of
-      Const ("HOL.times", Type ("fun", [Type ("nat", []),
+      Const (@{const_name HOL.times}, Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
       let
         val (i_nat, _, _) = interpret thy model
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Tools/res_clause.ML	Thu May 17 19:49:40 2007 +0200
@@ -103,15 +103,15 @@
 (*Provide readable names for the more common symbolic functions*)
 val const_trans_table =
       Symtab.make [("op =", "equal"),
-	  	   ("Orderings.less_eq", "lessequals"),
-		   ("Orderings.less", "less"),
+	  	   (@{const_name Orderings.less_eq}, "lessequals"),
+		   (@{const_name Orderings.less}, "less"),
 		   ("op &", "and"),
 		   ("op |", "or"),
-		   ("HOL.plus", "plus"),
-		   ("HOL.minus", "minus"),
-		   ("HOL.times", "times"),
-		   ("Divides.div", "div"),
-		   ("HOL.divide", "divide"),
+		   (@{const_name HOL.plus}, "plus"),
+		   (@{const_name HOL.minus}, "minus"),
+		   (@{const_name HOL.times}, "times"),
+		   (@{const_name Divides.div}, "div"),
+		   (@{const_name HOL.divide}, "divide"),
 		   ("op -->", "implies"),
 		   ("{}", "emptyset"),
 		   ("op :", "in"),
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/arith_data.ML	Thu May 17 19:49:40 2007 +0200
@@ -16,7 +16,7 @@
 
 (* mk_sum, mk_norm_sum *)
 
-val mk_plus = HOLogic.mk_binop "HOL.plus";
+val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
 
 fun mk_sum [] = HOLogic.zero
   | mk_sum [t] = t
@@ -30,7 +30,7 @@
 
 (* dest_sum *)
 
-val dest_plus = HOLogic.dest_bin "HOL.plus" HOLogic.natT;
+val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
 
 fun dest_sum tm =
   if HOLogic.is_zero tm then []
@@ -107,8 +107,8 @@
 structure LessCancelSums = CancelSumsFun
 (struct
   open Sum;
-  val mk_bal = HOLogic.mk_binrel "Orderings.less";
-  val dest_bal = HOLogic.dest_bin "Orderings.less" HOLogic.natT;
+  val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less};
+  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT;
   val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
 end);
 
@@ -117,8 +117,8 @@
 structure LeCancelSums = CancelSumsFun
 (struct
   open Sum;
-  val mk_bal = HOLogic.mk_binrel "Orderings.less_eq";
-  val dest_bal = HOLogic.dest_bin "Orderings.less_eq" HOLogic.natT;
+  val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq};
+  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT;
   val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
 end);
 
@@ -127,8 +127,8 @@
 structure DiffCancelSums = CancelSumsFun
 (struct
   open Sum;
-  val mk_bal = HOLogic.mk_binop "HOL.minus";
-  val dest_bal = HOLogic.dest_bin "HOL.minus" HOLogic.natT;
+  val mk_bal = HOLogic.mk_binop @{const_name HOL.minus};
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT;
   val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"};
 end);
 
@@ -283,17 +283,17 @@
 *)
 fun demult (inj_consts : (string * typ) list) : term * Rat.rat -> term option * Rat.rat =
 let
-  fun demult ((mC as Const ("HOL.times", _)) $ s $ t, m) = (
+  fun demult ((mC as Const (@{const_name HOL.times}, _)) $ s $ t, m) = (
     (case s of
-      Const ("Numeral.number_of", _) $ n =>
+      Const ("Numeral.number_class.number_of", _) $ n =>
         demult (t, Rat.mult m (Rat.rat_of_int (HOLogic.dest_numeral n)))
-    | Const ("HOL.uminus", _) $ (Const ("Numeral.number_of", _) $ n) =>
+    | Const (@{const_name HOL.uminus}, _) $ (Const ("Numeral.number_class.number_of", _) $ n) =>
         demult (t, Rat.mult m (Rat.rat_of_int (~(HOLogic.dest_numeral n))))
-    | Const ("Suc", _) $ _ =>
+    | Const (@{const_name Suc}, _) $ _ =>
         demult (t, Rat.mult m (Rat.rat_of_int (HOLogic.dest_nat s)))
-    | Const ("HOL.times", _) $ s1 $ s2 =>
+    | Const (@{const_name HOL.times}, _) $ s1 $ s2 =>
         demult (mC $ s1 $ (mC $ s2 $ t), m)
-    | Const ("HOL.divide", _) $ numt $ (Const ("Numeral.number_of", _) $ dent) =>
+    | Const (@{const_name HOL.divide}, _) $ numt $ (Const ("Numeral.number_class.number_of", _) $ dent) =>
         let
           val den = HOLogic.dest_numeral dent
         in
@@ -306,7 +306,7 @@
         atomult (mC, s, t, m)
     ) handle TERM _ => atomult (mC, s, t, m)
   )
-    | demult (atom as Const("HOL.divide", _) $ t $ (Const ("Numeral.number_of", _) $ dent), m) =
+    | demult (atom as Const(@{const_name HOL.divide}, _) $ t $ (Const ("Numeral.number_class.number_of", _) $ dent), m) =
       (let
         val den = HOLogic.dest_numeral dent
       in
@@ -316,14 +316,14 @@
           demult (t, Rat.mult m (Rat.inv (Rat.rat_of_int den)))
       end
         handle TERM _ => (SOME atom, m))
-    | demult (Const ("HOL.zero", _), m) = (NONE, Rat.zero)
-    | demult (Const ("HOL.one", _), m) = (NONE, m)
-    | demult (t as Const ("Numeral.number_of", _) $ n, m) =
+    | demult (Const (@{const_name HOL.zero}, _), m) = (NONE, Rat.zero)
+    | demult (Const (@{const_name HOL.one}, _), m) = (NONE, m)
+    | demult (t as Const ("Numeral.number_class.number_of", _) $ n, m) =
         ((NONE, Rat.mult m (Rat.rat_of_int (HOLogic.dest_numeral n)))
           handle TERM _ => (SOME t, m))
-    | demult (Const ("HOL.uminus", _) $ t, m) = demult (t, Rat.neg m)
+    | demult (Const (@{const_name HOL.uminus}, _) $ t, m) = demult (t, Rat.neg m)
     | demult (t as Const f $ x, m) =
-        (if f mem inj_consts then SOME x else SOME t, m)
+        (if member (op =) inj_consts f then SOME x else SOME t, m)
     | demult (atom, m) = (SOME atom, m)
 and
   atomult (mC, atom, t, m) = (
@@ -336,27 +336,27 @@
             ((term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat) option =
 let
   (* Turn term into list of summand * multiplicity plus a constant *)
-  fun poly (Const ("HOL.plus", _) $ s $ t, m : Rat.rat, pi : (term * Rat.rat) list * Rat.rat) =
+  fun poly (Const (@{const_name HOL.plus}, _) $ s $ t, m : Rat.rat, pi : (term * Rat.rat) list * Rat.rat) =
         poly (s, m, poly (t, m, pi))
-    | poly (all as Const ("HOL.minus", T) $ s $ t, m, pi) =
+    | poly (all as Const (@{const_name HOL.minus}, T) $ s $ t, m, pi) =
         if nT T then add_atom all m pi else poly (s, m, poly (t, Rat.neg m, pi))
-    | poly (all as Const ("HOL.uminus", T) $ t, m, pi) =
+    | poly (all as Const (@{const_name HOL.uminus}, T) $ t, m, pi) =
         if nT T then add_atom all m pi else poly (t, Rat.neg m, pi)
-    | poly (Const ("HOL.zero", _), _, pi) =
+    | poly (Const (@{const_name HOL.zero}, _), _, pi) =
         pi
-    | poly (Const ("HOL.one", _), m, (p, i)) =
+    | poly (Const (@{const_name HOL.one}, _), m, (p, i)) =
         (p, Rat.add i m)
-    | poly (Const ("Suc", _) $ t, m, (p, i)) =
+    | poly (Const (@{const_name Suc}, _) $ t, m, (p, i)) =
         poly (t, m, (p, Rat.add i m))
-    | poly (all as Const ("HOL.times", _) $ _ $ _, m, pi as (p, i)) =
+    | poly (all as Const (@{const_name HOL.times}, _) $ _ $ _, m, pi as (p, i)) =
         (case demult inj_consts (all, m) of
            (NONE,   m') => (p, Rat.add i m')
          | (SOME u, m') => add_atom u m' pi)
-    | poly (all as Const ("HOL.divide", _) $ _ $ _, m, pi as (p, i)) =
+    | poly (all as Const (@{const_name HOL.divide}, _) $ _ $ _, m, pi as (p, i)) =
         (case demult inj_consts (all, m) of
            (NONE,   m') => (p, Rat.add i m')
          | (SOME u, m') => add_atom u m' pi)
-    | poly (all as Const ("Numeral.number_of", Type(_,[_,T])) $ t, m, pi as (p, i)) =
+    | poly (all as Const ("Numeral.number_class.number_of", Type(_,[_,T])) $ t, m, pi as (p, i)) =
         (let val k = HOLogic.dest_numeral t
             val k2 = if k < 0 andalso T = HOLogic.natT then 0 else k
         in (p, Rat.add i (Rat.mult m (Rat.rat_of_int k2))) end
@@ -369,8 +369,8 @@
   val (q, j) = poly (rhs, Rat.one, ([], Rat.zero))
 in
   case rel of
-    "Orderings.less"    => SOME (p, i, "<", q, j)
-  | "Orderings.less_eq" => SOME (p, i, "<=", q, j)
+    @{const_name Orderings.less}    => SOME (p, i, "<", q, j)
+  | @{const_name Orderings.less_eq} => SOME (p, i, "<=", q, j)
   | "op ="              => SOME (p, i, "=", q, j)
   | _                   => NONE
 end handle Zero => NONE;
@@ -445,13 +445,13 @@
   case concl_of thm of _ $ (_ $ (_ $ lhs) $ _) => (
     (* Trueprop $ ((op =) $ (?P $ lhs) $ rhs) *)
     case head_of lhs of
-      Const (a, _) => a mem_string ["Orderings.max",
-                                    "Orderings.min",
-                                    "HOL.abs",
-                                    "HOL.minus",
+      Const (a, _) => member (op =) [@{const_name Orderings.max},
+                                    @{const_name Orderings.min},
+                                    @{const_name HOL.abs},
+                                    @{const_name HOL.minus},
                                     "IntDef.nat",
-                                    "Divides.mod",
-                                    "Divides.div"]
+                                    "Divides.div_class.mod",
+                                    "Divides.div_class.div"] a
     | _            => (warning ("Lin. Arith.: wrong format for split rule " ^
                                  Display.string_of_thm thm);
                        false))
@@ -515,12 +515,12 @@
     (* ignore all but the first possible split *)
     case strip_comb split_term of
     (* ?P (max ?i ?j) = ((?i <= ?j --> ?P ?j) & (~ ?i <= ?j --> ?P ?i)) *)
-      (Const ("Orderings.max", _), [t1, t2]) =>
+      (Const (@{const_name Orderings.max}, _), [t1, t2]) =>
       let
         val rev_terms     = rev terms
         val terms1        = map (subst_term [(split_term, t1)]) rev_terms
         val terms2        = map (subst_term [(split_term, t2)]) rev_terms
-        val t1_leq_t2     = Const ("Orderings.less_eq",
+        val t1_leq_t2     = Const (@{const_name Orderings.less_eq},
                                     split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
         val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
         val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
@@ -530,12 +530,12 @@
         SOME [(Ts, subgoal1), (Ts, subgoal2)]
       end
     (* ?P (min ?i ?j) = ((?i <= ?j --> ?P ?i) & (~ ?i <= ?j --> ?P ?j)) *)
-    | (Const ("Orderings.min", _), [t1, t2]) =>
+    | (Const (@{const_name Orderings.min}, _), [t1, t2]) =>
       let
         val rev_terms     = rev terms
         val terms1        = map (subst_term [(split_term, t1)]) rev_terms
         val terms2        = map (subst_term [(split_term, t2)]) rev_terms
-        val t1_leq_t2     = Const ("Orderings.less_eq",
+        val t1_leq_t2     = Const (@{const_name Orderings.less_eq},
                                     split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
         val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
         val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
@@ -545,16 +545,16 @@
         SOME [(Ts, subgoal1), (Ts, subgoal2)]
       end
     (* ?P (abs ?a) = ((0 <= ?a --> ?P ?a) & (?a < 0 --> ?P (- ?a))) *)
-    | (Const ("HOL.abs", _), [t1]) =>
+    | (Const (@{const_name HOL.abs}, _), [t1]) =>
       let
         val rev_terms   = rev terms
         val terms1      = map (subst_term [(split_term, t1)]) rev_terms
-        val terms2      = map (subst_term [(split_term, Const ("HOL.uminus",
+        val terms2      = map (subst_term [(split_term, Const (@{const_name HOL.uminus},
                             split_type --> split_type) $ t1)]) rev_terms
-        val zero        = Const ("HOL.zero", split_type)
-        val zero_leq_t1 = Const ("Orderings.less_eq",
+        val zero        = Const (@{const_name HOL.zero}, split_type)
+        val zero_leq_t1 = Const (@{const_name Orderings.less_eq},
                             split_type --> split_type --> HOLogic.boolT) $ zero $ t1
-        val t1_lt_zero  = Const ("Orderings.less",
+        val t1_lt_zero  = Const (@{const_name Orderings.less},
                             split_type --> split_type --> HOLogic.boolT) $ t1 $ zero
         val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1    = (HOLogic.mk_Trueprop zero_leq_t1) :: terms1 @ [not_false]
@@ -563,22 +563,22 @@
         SOME [(Ts, subgoal1), (Ts, subgoal2)]
       end
     (* ?P (?a - ?b) = ((?a < ?b --> ?P 0) & (ALL d. ?a = ?b + d --> ?P d)) *)
-    | (Const ("HOL.minus", _), [t1, t2]) =>
+    | (Const (@{const_name HOL.minus}, _), [t1, t2]) =>
       let
         (* "d" in the above theorem becomes a new bound variable after NNF   *)
         (* transformation, therefore some adjustment of indices is necessary *)
         val rev_terms       = rev terms
-        val zero            = Const ("HOL.zero", split_type)
+        val zero            = Const (@{const_name HOL.zero}, split_type)
         val d               = Bound 0
         val terms1          = map (subst_term [(split_term, zero)]) rev_terms
         val terms2          = map (subst_term [(incr_boundvars 1 split_term, d)])
                                 (map (incr_boundvars 1) rev_terms)
         val t1'             = incr_boundvars 1 t1
         val t2'             = incr_boundvars 1 t2
-        val t1_lt_t2        = Const ("Orderings.less",
+        val t1_lt_t2        = Const (@{const_name Orderings.less},
                                 split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
         val t1_eq_t2_plus_d = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
-                                (Const ("HOL.plus",
+                                (Const (@{const_name HOL.plus},
                                   split_type --> split_type --> split_type) $ t2' $ d)
         val not_false       = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1        = (HOLogic.mk_Trueprop t1_lt_t2) :: terms1 @ [not_false]
@@ -590,8 +590,8 @@
     | (Const ("IntDef.nat", _), [t1]) =>
       let
         val rev_terms   = rev terms
-        val zero_int    = Const ("HOL.zero", HOLogic.intT)
-        val zero_nat    = Const ("HOL.zero", HOLogic.natT)
+        val zero_int    = Const (@{const_name HOL.zero}, HOLogic.intT)
+        val zero_nat    = Const (@{const_name HOL.zero}, HOLogic.natT)
         val n           = Bound 0
         val terms1      = map (subst_term [(incr_boundvars 1 split_term, n)])
                             (map (incr_boundvars 1) rev_terms)
@@ -599,7 +599,7 @@
         val t1'         = incr_boundvars 1 t1
         val t1_eq_int_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
                             (Const ("IntDef.int", HOLogic.natT --> HOLogic.intT) $ n)
-        val t1_lt_zero  = Const ("Orderings.less",
+        val t1_lt_zero  = Const (@{const_name Orderings.less},
                             HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
         val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1    = (HOLogic.mk_Trueprop t1_eq_int_n) :: terms1 @ [not_false]
@@ -610,10 +610,10 @@
     (* "?P ((?n::nat) mod (number_of ?k)) =
          ((number_of ?k = 0 --> ?P ?n) & (~ (number_of ?k = 0) -->
            (ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P j))) *)
-    | (Const ("Divides.mod", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
+    | (Const ("Divides.div_class.mod", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
       let
         val rev_terms               = rev terms
-        val zero                    = Const ("HOL.zero", split_type)
+        val zero                    = Const (@{const_name HOL.zero}, split_type)
         val i                       = Bound 1
         val j                       = Bound 0
         val terms1                  = map (subst_term [(split_term, t1)]) rev_terms
@@ -625,11 +625,11 @@
                                         split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
         val t2_neq_zero             = HOLogic.mk_not (Const ("op =",
                                         split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
-        val j_lt_t2                 = Const ("Orderings.less",
+        val j_lt_t2                 = Const (@{const_name Orderings.less},
                                         split_type --> split_type--> HOLogic.boolT) $ j $ t2'
         val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
-                                       (Const ("HOL.plus", split_type --> split_type --> split_type) $
-                                         (Const ("HOL.times",
+                                       (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
+                                         (Const (@{const_name HOL.times},
                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
         val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
@@ -642,10 +642,10 @@
     (* "?P ((?n::nat) div (number_of ?k)) =
          ((number_of ?k = 0 --> ?P 0) & (~ (number_of ?k = 0) -->
            (ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P i))) *)
-    | (Const ("Divides.div", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
+    | (Const ("Divides.div_class.div", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
       let
         val rev_terms               = rev terms
-        val zero                    = Const ("HOL.zero", split_type)
+        val zero                    = Const (@{const_name HOL.zero}, split_type)
         val i                       = Bound 1
         val j                       = Bound 0
         val terms1                  = map (subst_term [(split_term, zero)]) rev_terms
@@ -657,11 +657,11 @@
                                         split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
         val t2_neq_zero             = HOLogic.mk_not (Const ("op =",
                                         split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
-        val j_lt_t2                 = Const ("Orderings.less",
+        val j_lt_t2                 = Const (@{const_name Orderings.less},
                                         split_type --> split_type--> HOLogic.boolT) $ j $ t2'
         val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
-                                       (Const ("HOL.plus", split_type --> split_type --> split_type) $
-                                         (Const ("HOL.times",
+                                       (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
+                                         (Const (@{const_name HOL.times},
                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
         val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
@@ -677,11 +677,11 @@
             (ALL i j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j --> ?P j)) &
           (neg (number_of ?k) -->
             (ALL i j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j --> ?P j))) *)
-    | (Const ("Divides.mod",
+    | (Const ("Divides.div_class.mod",
         Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
       let
         val rev_terms               = rev terms
-        val zero                    = Const ("HOL.zero", split_type)
+        val zero                    = Const (@{const_name HOL.zero}, split_type)
         val i                       = Bound 1
         val j                       = Bound 0
         val terms1                  = map (subst_term [(split_term, t1)]) rev_terms
@@ -692,20 +692,20 @@
         val iszero_t2               = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2
         val neg_minus_k             = Const ("IntDef.neg", split_type --> HOLogic.boolT) $
                                         (number_of $
-                                          (Const ("HOL.uminus",
+                                          (Const (@{const_name HOL.uminus},
                                             HOLogic.intT --> HOLogic.intT) $ k'))
-        val zero_leq_j              = Const ("Orderings.less_eq",
+        val zero_leq_j              = Const (@{const_name Orderings.less_eq},
                                         split_type --> split_type --> HOLogic.boolT) $ zero $ j
-        val j_lt_t2                 = Const ("Orderings.less",
+        val j_lt_t2                 = Const (@{const_name Orderings.less},
                                         split_type --> split_type--> HOLogic.boolT) $ j $ t2'
         val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
-                                       (Const ("HOL.plus", split_type --> split_type --> split_type) $
-                                         (Const ("HOL.times",
+                                       (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
+                                         (Const (@{const_name HOL.times},
                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
         val neg_t2                  = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ t2'
-        val t2_lt_j                 = Const ("Orderings.less",
+        val t2_lt_j                 = Const (@{const_name Orderings.less},
                                         split_type --> split_type--> HOLogic.boolT) $ t2' $ j
-        val j_leq_zero              = Const ("Orderings.less_eq",
+        val j_leq_zero              = Const (@{const_name Orderings.less_eq},
                                         split_type --> split_type --> HOLogic.boolT) $ j $ zero
         val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1                = (HOLogic.mk_Trueprop iszero_t2) :: terms1 @ [not_false]
@@ -729,11 +729,11 @@
             (ALL i. (EX j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j) --> ?P i)) &
           (neg (number_of ?k) -->
             (ALL i. (EX j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j) --> ?P i))) *)
-    | (Const ("Divides.div",
+    | (Const ("Divides.div_class.div",
         Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
       let
         val rev_terms               = rev terms
-        val zero                    = Const ("HOL.zero", split_type)
+        val zero                    = Const (@{const_name HOL.zero}, split_type)
         val i                       = Bound 1
         val j                       = Bound 0
         val terms1                  = map (subst_term [(split_term, zero)]) rev_terms
@@ -744,21 +744,21 @@
         val iszero_t2               = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2
         val neg_minus_k             = Const ("IntDef.neg", split_type --> HOLogic.boolT) $
                                         (number_of $
-                                          (Const ("HOL.uminus",
+                                          (Const (@{const_name HOL.uminus},
                                             HOLogic.intT --> HOLogic.intT) $ k'))
-        val zero_leq_j              = Const ("Orderings.less_eq",
+        val zero_leq_j              = Const (@{const_name Orderings.less_eq},
                                         split_type --> split_type --> HOLogic.boolT) $ zero $ j
-        val j_lt_t2                 = Const ("Orderings.less",
+        val j_lt_t2                 = Const (@{const_name Orderings.less},
                                         split_type --> split_type--> HOLogic.boolT) $ j $ t2'
         val t1_eq_t2_times_i_plus_j = Const ("op =",
                                         split_type --> split_type --> HOLogic.boolT) $ t1' $
-                                       (Const ("HOL.plus", split_type --> split_type --> split_type) $
-                                         (Const ("HOL.times",
+                                       (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
+                                         (Const (@{const_name HOL.times},
                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
         val neg_t2                  = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ t2'
-        val t2_lt_j                 = Const ("Orderings.less",
+        val t2_lt_j                 = Const (@{const_name Orderings.less},
                                         split_type --> split_type--> HOLogic.boolT) $ t2' $ j
-        val j_leq_zero              = Const ("Orderings.less_eq",
+        val j_leq_zero              = Const (@{const_name Orderings.less_eq},
                                         split_type --> split_type --> HOLogic.boolT) $ j $ zero
         val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1                = (HOLogic.mk_Trueprop iszero_t2) :: terms1 @ [not_false]
@@ -1009,24 +1009,24 @@
     val r = #prop(rep_thm thm);
   in
     case r of
-      Tr $ ((c as Const("Orderings.less_eq",T)) $ s $ t) =>
+      Tr $ ((c as Const(@{const_name Orderings.less_eq},T)) $ s $ t) =>
         let val r' = Tr $ (c $ t $ s)
         in
           case Library.find_first (prp r') prems of
             NONE =>
-              let val r' = Tr $ (HOLogic.Not $ (Const("Orderings.less",T) $ s $ t))
+              let val r' = Tr $ (HOLogic.Not $ (Const(@{const_name Orderings.less},T) $ s $ t))
               in case Library.find_first (prp r') prems of
                    NONE => []
                  | SOME thm' => [(thm' RS not_lessD) RS (thm RS antisym)]
               end
           | SOME thm' => [thm' RS (thm RS antisym)]
         end
-    | Tr $ (Const("Not",_) $ (Const("Orderings.less",T) $ s $ t)) =>
-        let val r' = Tr $ (Const("Orderings.less_eq",T) $ s $ t)
+    | Tr $ (Const("Not",_) $ (Const(@{const_name Orderings.less},T) $ s $ t)) =>
+        let val r' = Tr $ (Const(@{const_name Orderings.less_eq},T) $ s $ t)
         in
           case Library.find_first (prp r') prems of
             NONE =>
-              let val r' = Tr $ (HOLogic.Not $ (Const("Orderings.less",T) $ t $ s))
+              let val r' = Tr $ (HOLogic.Not $ (Const(@{const_name Orderings.less},T) $ t $ s))
               in case Library.find_first (prp r') prems of
                    NONE => []
                  | SOME thm' =>
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/ex/Binary.thy
--- a/src/HOL/ex/Binary.thy	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/ex/Binary.thy	Thu May 17 19:49:40 2007 +0200
@@ -25,8 +25,8 @@
     | dest_bit (Const ("True", _)) = 1
     | dest_bit t = raise TERM ("dest_bit", [t]);
 
-  fun dest_binary (Const ("HOL.zero", Type ("nat", _))) = 0
-    | dest_binary (Const ("HOL.one", Type ("nat", _))) = 1
+  fun dest_binary (Const (@{const_name HOL.zero}, Type ("nat", _))) = 0
+    | dest_binary (Const (@{const_name HOL.one}, Type ("nat", _))) = 1
     | dest_binary (Const ("Binary.bit", _) $ bs $ b) =
         2 * dest_binary bs + IntInf.fromInt (dest_bit b)
     | dest_binary t = raise TERM ("dest_binary", [t]);
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/ex/svc_funcs.ML
--- a/src/HOL/ex/svc_funcs.ML	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/ex/svc_funcs.ML	Thu May 17 19:49:40 2007 +0200
@@ -112,8 +112,8 @@
                          b1 orelse b2)
                      end
                  else (*might be numeric equality*) (t, is_intnat T)
-           | Const("Orderings.less", Type ("fun", [T,_]))  => (t, is_intnat T)
-           | Const("Orderings.less_eq", Type ("fun", [T,_])) => (t, is_intnat T)
+           | Const(@{const_name Orderings.less}, Type ("fun", [T,_]))  => (t, is_intnat T)
+           | Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) => (t, is_intnat T)
            | _ => (t, false)
          end
    in #1 o tag end;
@@ -151,38 +151,38 @@
     (*translation of a literal*)
     val lit = snd o HOLogic.dest_number;
     (*translation of a literal expression [no variables]*)
-    fun litExp (Const("HOL.plus", T) $ x $ y) =
+    fun litExp (Const(@{const_name HOL.plus}, T) $ x $ y) =
           if is_numeric_op T then (litExp x) + (litExp y)
           else fail t
-      | litExp (Const("HOL.minus", T) $ x $ y) =
+      | litExp (Const(@{const_name HOL.minus}, T) $ x $ y) =
           if is_numeric_op T then (litExp x) - (litExp y)
           else fail t
-      | litExp (Const("HOL.times", T) $ x $ y) =
+      | litExp (Const(@{const_name HOL.times}, T) $ x $ y) =
           if is_numeric_op T then (litExp x) * (litExp y)
           else fail t
-      | litExp (Const("HOL.uminus", T) $ x)   =
+      | litExp (Const(@{const_name HOL.uminus}, T) $ x)   =
           if is_numeric_op T then ~(litExp x)
           else fail t
       | litExp t = lit t
                    handle Match => fail t
     (*translation of a real/rational expression*)
     fun suc t = Interp("+", [Int 1, t])
-    fun tm (Const("Suc", T) $ x) = suc (tm x)
-      | tm (Const("HOL.plus", T) $ x $ y) =
+    fun tm (Const(@{const_name Suc}, T) $ x) = suc (tm x)
+      | tm (Const(@{const_name HOL.plus}, T) $ x $ y) =
           if is_numeric_op T then Interp("+", [tm x, tm y])
           else fail t
-      | tm (Const("HOL.minus", T) $ x $ y) =
+      | tm (Const(@{const_name HOL.minus}, T) $ x $ y) =
           if is_numeric_op T then
               Interp("+", [tm x, Interp("*", [Int ~1, tm y])])
           else fail t
-      | tm (Const("HOL.times", T) $ x $ y) =
+      | tm (Const(@{const_name HOL.times}, T) $ x $ y) =
           if is_numeric_op T then Interp("*", [tm x, tm y])
           else fail t
-      | tm (Const("RealDef.rinv", T) $ x) =
+      | tm (Const(@{const_name HOL.inverse}, T) $ x) =
           if domain_type T = HOLogic.realT then
               Rat(1, litExp x)
           else fail t
-      | tm (Const("HOL.uminus", T) $ x) =
+      | tm (Const(@{const_name HOL.uminus}, T) $ x) =
           if is_numeric_op T then Interp("*", [Int ~1, tm x])
           else fail t
       | tm t = Int (lit t)
@@ -216,13 +216,13 @@
                    else fail t
             end
         (*inequalities: possible types are nat, int, real*)
-      | fm pos (t as Const("Orderings.less",  Type ("fun", [T,_])) $ x $ y) =
+      | fm pos (t as Const(@{const_name Orderings.less},  Type ("fun", [T,_])) $ x $ y) =
             if not pos orelse T = HOLogic.realT then
                 Buildin("<", [tm x, tm y])
             else if is_intnat T then
                 Buildin("<=", [suc (tm x), tm y])
             else fail t
-      | fm pos (t as Const("Orderings.less_eq",  Type ("fun", [T,_])) $ x $ y) =
+      | fm pos (t as Const(@{const_name Orderings.less_eq},  Type ("fun", [T,_])) $ x $ y) =
             if pos orelse T = HOLogic.realT then
                 Buildin("<=", [tm x, tm y])
             else if is_intnat T then
diff -r 5f82c5f8478e -r d4f3b015b50b src/HOL/ex/svc_oracle.ML
--- a/src/HOL/ex/svc_oracle.ML	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/ex/svc_oracle.ML	Thu May 17 19:49:40 2007 +0200
@@ -41,27 +41,27 @@
                       SOME v => v
                     | NONE   => insert t)
     (*abstraction of a numeric literal*)
-    fun lit (t as Const("0", _)) = t
-      | lit (t as Const("1", _)) = t
-      | lit (t as Const("Numeral.number_of", _) $ w) = t
+    fun lit (t as Const(@{const_name HOL.zero}, _)) = t
+      | lit (t as Const(@{const_name HOL.one}, _)) = t
+      | lit (t as Const(@{const_name Numeral.number_of}, _) $ w) = t
       | lit t = replace t
     (*abstraction of a real/rational expression*)
-    fun rat ((c as Const("HOL.plus", _)) $ x $ y) = c $ (rat x) $ (rat y)
-      | rat ((c as Const("HOL.minus", _)) $ x $ y) = c $ (rat x) $ (rat y)
-      | rat ((c as Const("HOL.divide", _)) $ x $ y) = c $ (rat x) $ (rat y)
-      | rat ((c as Const("HOL.times", _)) $ x $ y) = c $ (rat x) $ (rat y)
-      | rat ((c as Const("HOL.uminus", _)) $ x) = c $ (rat x)
+    fun rat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
+      | rat ((c as Const(@{const_name HOL.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
+      | rat ((c as Const(@{const_name HOL.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y)
+      | rat ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (rat x) $ (rat y)
+      | rat ((c as Const(@{const_name HOL.uminus}, _)) $ x) = c $ (rat x)
       | rat t = lit t
     (*abstraction of an integer expression: no div, mod*)
-    fun int ((c as Const("HOL.plus", _)) $ x $ y) = c $ (int x) $ (int y)
-      | int ((c as Const("HOL.minus", _)) $ x $ y) = c $ (int x) $ (int y)
-      | int ((c as Const("HOL.times", _)) $ x $ y) = c $ (int x) $ (int y)
-      | int ((c as Const("HOL.uminus", _)) $ x) = c $ (int x)
+    fun int ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (int x) $ (int y)
+      | int ((c as Const(@{const_name HOL.minus}, _)) $ x $ y) = c $ (int x) $ (int y)
+      | int ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (int x) $ (int y)
+      | int ((c as Const(@{const_name HOL.uminus}, _)) $ x) = c $ (int x)
       | int t = lit t
     (*abstraction of a natural number expression: no minus*)
-    fun nat ((c as Const("HOL.plus", _)) $ x $ y) = c $ (nat x) $ (nat y)
-      | nat ((c as Const("HOL.times", _)) $ x $ y) = c $ (nat x) $ (nat y)
-      | nat ((c as Const("Suc", _)) $ x) = c $ (nat x)
+    fun nat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (nat x) $ (nat y)
+      | nat ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (nat x) $ (nat y)
+      | nat ((c as Const(@{const_name Suc}, _)) $ x) = c $ (nat x)
       | nat t = lit t
     (*abstraction of a relation: =, <, <=*)
     fun rel (T, c $ x $ y) =
@@ -78,8 +78,8 @@
       | fm ((c as Const("True", _))) = c
       | fm ((c as Const("False", _))) = c
       | fm (t as Const("op =",  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
-      | fm (t as Const("Orderings.less",  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
-      | fm (t as Const("Orderings.less_eq", 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("Trueprop", _)) $ p) = c $ (fm p)
diff -r 5f82c5f8478e -r d4f3b015b50b src/Provers/Arith/abel_cancel.ML
--- a/src/Provers/Arith/abel_cancel.ML	Thu May 17 19:49:21 2007 +0200
+++ b/src/Provers/Arith/abel_cancel.ML	Thu May 17 19:49:40 2007 +0200
@@ -28,29 +28,29 @@
 
 (* FIXME dependent on abstract syntax *)
 
-fun zero t = Const ("HOL.zero", t);
-fun minus t = Const ("HOL.uminus", t --> t);
+fun zero t = Const (@{const_name HOL.zero}, t);
+fun minus t = Const (@{const_name HOL.uminus}, t --> t);
 
-fun add_terms pos (Const ("HOL.plus", _) $ x $ y, ts) =
+fun add_terms pos (Const (@{const_name HOL.plus}, _) $ x $ y, ts) =
       add_terms pos (x, add_terms pos (y, ts))
-  | add_terms pos (Const ("HOL.minus", _) $ x $ y, ts) =
+  | add_terms pos (Const (@{const_name HOL.minus}, _) $ x $ y, ts) =
       add_terms pos (x, add_terms (not pos) (y, ts))
-  | add_terms pos (Const ("HOL.uminus", _) $ x, ts) =
+  | add_terms pos (Const (@{const_name HOL.uminus}, _) $ x, ts) =
       add_terms (not pos) (x, ts)
   | add_terms pos (x, ts) = (pos,x) :: ts;
 
 fun terms fml = add_terms true (fml, []);
 
-fun zero1 pt (u as (c as Const("HOL.plus",_)) $ x $ y) =
+fun zero1 pt (u as (c as Const(@{const_name HOL.plus},_)) $ x $ y) =
       (case zero1 pt x of NONE => (case zero1 pt y of NONE => NONE
                                    | SOME z => SOME(c $ x $ z))
        | SOME z => SOME(c $ z $ y))
-  | zero1 (pos,t) (u as (c as Const("HOL.minus",_)) $ x $ y) =
+  | zero1 (pos,t) (u as (c as Const(@{const_name HOL.minus},_)) $ x $ y) =
       (case zero1 (pos,t) x of
          NONE => (case zero1 (not pos,t) y of NONE => NONE
                   | SOME z => SOME(c $ x $ z))
        | SOME z => SOME(c $ z $ y))
-  | zero1 (pos,t) (u as (c as Const("HOL.uminus",_)) $ x) =
+  | zero1 (pos,t) (u as (c as Const(@{const_name HOL.uminus},_)) $ x) =
       (case zero1 (not pos,t) x of NONE => NONE
        | SOME z => SOME(c $ z))
   | zero1 (pos,t) u =
@@ -71,7 +71,7 @@
 fun cancel t =
   let
     val c $ lhs $ rhs = t
-    val opp = case c of Const("HOL.plus",_) => true | _ => false;
+    val opp = case c of Const(@{const_name HOL.plus},_) => true | _ => false;
     val (pos,l) = find_common opp (terms lhs) (terms rhs)
     val posr = if opp then not pos else pos
     val t' = c $ (the(zero1 (pos,l) lhs)) $ (the(zero1 (posr,l) rhs))
diff -r 5f82c5f8478e -r d4f3b015b50b src/Provers/Arith/assoc_fold.ML
--- a/src/Provers/Arith/assoc_fold.ML	Thu May 17 19:49:21 2007 +0200
+++ b/src/Provers/Arith/assoc_fold.ML	Thu May 17 19:49:40 2007 +0200
@@ -30,7 +30,7 @@
 (*Separate the literals from the other terms being combined*)
 fun sift_terms plus (t, (lits,others)) =
   (case t of
-    Const("Numeral.number_of", _) $ _ =>       (* FIXME logic dependent *)
+    Const (@{const_name Numeral.number_of}, _) $ _ =>       (* FIXME logic dependent *)
       (t::lits, others)         (*new literal*)
   | (f as Const _) $ x $ y =>
       if f = plus
diff -r 5f82c5f8478e -r d4f3b015b50b src/Provers/Arith/cancel_div_mod.ML
--- a/src/Provers/Arith/cancel_div_mod.ML	Thu May 17 19:49:21 2007 +0200
+++ b/src/Provers/Arith/cancel_div_mod.ML	Thu May 17 19:49:40 2007 +0200
@@ -6,8 +6,8 @@
 
   A + n*(m div n) + B + (m mod n) + C  ==  A + B + C + m
 
-FIXME: Is parameterized but assumes for simplicity that + and * are called
-"HOL.plus" and "HOL.minus"
+FIXME: Is parameterized but assumes for simplicity that + and * are named
+HOL.plus and HOL.minus
 *)
 
 signature CANCEL_DIV_MOD_DATA =
@@ -35,12 +35,12 @@
 functor CancelDivModFun(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD =
 struct
 
-fun coll_div_mod (Const("HOL.plus",_) $ s $ t) dms =
+fun coll_div_mod (Const(@{const_name HOL.plus},_) $ s $ t) dms =
       coll_div_mod t (coll_div_mod s dms)
-  | coll_div_mod (Const("HOL.times",_) $ m $ (Const(d,_) $ s $ n))
+  | coll_div_mod (Const(@{const_name HOL.times},_) $ m $ (Const(d,_) $ s $ n))
                  (dms as (divs,mods)) =
       if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms
-  | coll_div_mod (Const("HOL.times",_) $ (Const(d,_) $ s $ n) $ m)
+  | coll_div_mod (Const(@{const_name HOL.times},_) $ (Const(d,_) $ s $ n) $ m)
                  (dms as (divs,mods)) =
       if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms
   | coll_div_mod (Const(m,_) $ s $ n) (dms as (divs,mods)) =
@@ -56,8 +56,8 @@
    ==> thesis by transitivity
 *)
 
-val mk_plus = Data.mk_binop "HOL.plus"
-val mk_times = Data.mk_binop "HOL.times"
+val mk_plus = Data.mk_binop @{const_name HOL.plus};
+val mk_times = Data.mk_binop @{const_name HOL.times};
 
 fun rearrange t pq =
   let val ts = Data.dest_sum t;
diff -r 5f82c5f8478e -r d4f3b015b50b src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Thu May 17 19:49:21 2007 +0200
+++ b/src/Pure/Tools/class_package.ML	Thu May 17 19:49:40 2007 +0200
@@ -97,22 +97,27 @@
   let
     val superclasses = map (Sign.certify_class thy) raw_superclasses;
     val consts = (map o apfst o apsnd) (Sign.certify_typ thy) raw_consts;
+    val prefix = Logic.const_of_class name;
+    fun mk_const_name c = NameSpace.map_base (NameSpace.append prefix)
+      (Sign.full_name thy c);
     fun add_const ((c, ty), syn) =
       Sign.add_consts_authentic [(c, ty, syn)]
-      #> pair (Sign.full_name thy c, ty);
+      #> pair (mk_const_name c, ty);
     fun mk_axioms cs thy =
       raw_dep_axioms thy cs
       |> (map o apsnd o map) (Sign.cert_prop thy)
       |> rpair thy;
     fun add_constraint class (c, ty) =
-      Sign.add_const_constraint_i (c, SOME (Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty));
+      Sign.add_const_constraint_i (c, SOME
+        (Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty));
   in
     thy
-    (* |> Theory.add_path name *)
+    |> Theory.add_path prefix
     |> fold_map add_const consts
-    (* ||> Theory.restore_naming thy *)
+    ||> Theory.restore_naming thy
     |-> (fn cs => mk_axioms cs
-    #-> (fn axioms_prop => AxClass.define_class (name, superclasses) (map fst cs @ other_consts) axioms_prop
+    #-> (fn axioms_prop => AxClass.define_class (name, superclasses)
+           (map fst cs @ other_consts) axioms_prop
     #-> (fn class => `(fn thy => AxClass.get_definition thy class)
     #-> (fn {intro, axioms, ...} => fold (add_constraint class) cs
     #> pair (class, ((intro, (map Thm.prop_of axioms, axioms)), cs))))))