diff -r 8f0e07d7cf92 -r 95e84d2c9f2c src/HOL/OrderedGroup.ML
--- a/src/HOL/OrderedGroup.ML	Fri Jul 14 14:19:48 2006 +0200
+++ b/src/HOL/OrderedGroup.ML	Fri Jul 14 14:37:15 2006 +0200
@@ -1,6 +1,6 @@
 (*  Title:      HOL/OrderedGroup.ML
     ID:         $Id$
-    Author:     Steven Obua, Tobias Nipkow, Technische Universitaet Mnchen
+    Author:     Steven Obua, Tobias Nipkow, Technische Universitaet Muenchen
 *)
 
 structure ab_group_add_cancel_data :> ABEL_CANCEL  = 
@@ -8,7 +8,8 @@
 
 (*** Term order for abelian groups ***)
 
-fun agrp_ord a = find_index (fn a' => a = a') ["0", "HOL.plus", "HOL.uminus", "HOL.minus"];
+fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a') ["0", "HOL.plus", "HOL.uminus", "HOL.minus"]
+  | agrp_ord _ = ~1;
 
 fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS);