--- 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