src/HOL/OrderedGroup.thy
changeset 22997 d4f3b015b50b
parent 22986 d21d3539f6bb
child 23085 fd30d75a6614
     1.1 --- a/src/HOL/OrderedGroup.thy	Thu May 17 19:49:21 2007 +0200
     1.2 +++ b/src/HOL/OrderedGroup.thy	Thu May 17 19:49:40 2007 +0200
     1.3 @@ -1058,7 +1058,8 @@
     1.4  (* term order for abelian groups *)
     1.5  
     1.6  fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a')
     1.7 -      ["HOL.zero", "HOL.plus", "HOL.uminus", "HOL.minus"]
     1.8 +      [@{const_name HOL.zero}, @{const_name HOL.plus},
     1.9 +        @{const_name HOL.uminus}, @{const_name HOL.minus}]
    1.10    | agrp_ord _ = ~1;
    1.11  
    1.12  fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS);
    1.13 @@ -1067,9 +1068,9 @@
    1.14    val ac1 = mk_meta_eq @{thm add_assoc};
    1.15    val ac2 = mk_meta_eq @{thm add_commute};
    1.16    val ac3 = mk_meta_eq @{thm add_left_commute};
    1.17 -  fun solve_add_ac thy _ (_ $ (Const ("HOL.plus",_) $ _ $ _) $ _) =
    1.18 +  fun solve_add_ac thy _ (_ $ (Const (@{const_name HOL.plus},_) $ _ $ _) $ _) =
    1.19          SOME ac1
    1.20 -    | solve_add_ac thy _ (_ $ x $ (Const ("HOL.plus",_) $ y $ z)) =
    1.21 +    | solve_add_ac thy _ (_ $ x $ (Const (@{const_name HOL.plus},_) $ y $ z)) =
    1.22          if termless_agrp (y, x) then SOME ac3 else NONE
    1.23      | solve_add_ac thy _ (_ $ x $ y) =
    1.24          if termless_agrp (y, x) then SOME ac2 else NONE