# HG changeset patch
# User ballarin
# Date 1152880635 -7200
# Node ID 95e84d2c9f2c5103af7b722830eb5655351fb1d4
# Parent  8f0e07d7cf92b8666530c508bac1d1c43f717b7d
Term.term_lpo takes order on terms rather than strings as argument.

diff -r 8f0e07d7cf92 -r 95e84d2c9f2c src/HOL/Algebra/abstract/order.ML
--- a/src/HOL/Algebra/abstract/order.ML	Fri Jul 14 14:19:48 2006 +0200
+++ b/src/HOL/Algebra/abstract/order.ML	Fri Jul 14 14:37:15 2006 +0200
@@ -7,8 +7,9 @@
 
 (*** Term order for commutative rings ***)
 
-fun ring_ord a =
-  find_index (fn a' => a = a') ["0", "HOL.plus", "HOL.uminus", "HOL.minus", "1", "HOL.times"];
+fun ring_ord (Const (a, _)) =
+    find_index (fn a' => a = a') ["0", "HOL.plus", "HOL.uminus", "HOL.minus", "1", "HOL.times"]
+  | ring_ord _ = ~1;
 
 fun termless_ring (a, b) = (Term.term_lpo ring_ord (a, b) = LESS);
 
diff -r 8f0e07d7cf92 -r 95e84d2c9f2c src/HOL/Algebra/ringsimp.ML
--- a/src/HOL/Algebra/ringsimp.ML	Fri Jul 14 14:19:48 2006 +0200
+++ b/src/HOL/Algebra/ringsimp.ML	Fri Jul 14 14:37:15 2006 +0200
@@ -7,9 +7,10 @@
 
 (*** Term order for commutative rings ***)
 
-fun ring_ord a =
-  find_index_eq a ["CRing.ring.zero", "CRing.ring.add", "CRing.a_inv",
-  "CRing.minus", "Group.monoid.one", "Group.monoid.mult"];
+fun ring_ord (Const (a, _)) =
+    find_index_eq a ["CRing.ring.zero", "CRing.ring.add", "CRing.a_inv",
+      "CRing.minus", "Group.monoid.one", "Group.monoid.mult"]
+  | ring_ord _ = ~1;
 
 fun termless_ring (a, b) = (Term.term_lpo ring_ord (a, b) = LESS);
 
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);
 
diff -r 8f0e07d7cf92 -r 95e84d2c9f2c src/Pure/term.ML
--- a/src/Pure/term.ML	Fri Jul 14 14:19:48 2006 +0200
+++ b/src/Pure/term.ML	Fri Jul 14 14:37:15 2006 +0200
@@ -172,7 +172,7 @@
   val term_ord: term * term -> order
   val hd_ord: term * term -> order
   val termless: term * term -> bool
-  val term_lpo: (string -> int) -> term * term -> order
+  val term_lpo: (term -> int) -> term * term -> order
   val match_bvars: (term * term) * (string * string) list -> (string * string) list
   val rename_abs: term -> term -> term -> term option
   val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
@@ -646,23 +646,26 @@
   Without variables.  Const, Var, Bound, Free and Abs are treated all as
   constants.
 
-  f_ord maps strings to integers and serves two purposes:
+  f_ord maps terms to integers and serves two purposes:
   - Predicate on constant symbols.  Those that are not recognised by f_ord
     must be mapped to ~1.
   - Order on the recognised symbols.  These must be mapped to distinct
     integers >= 0.
-
+  The argument of f_ord is never an application.
 *)
 
 local
-fun dest_hd f_ord (Const (a, T)) =
-      let val ord = f_ord a in
-        if ord = ~1 then ((1, ((a, 0), T)), 0) else ((0, (("", ord), T)), 0)
+
+fun unrecognized (Const (a, T)) = ((1, ((a, 0), T)), 0)
+  | unrecognized (Free (a, T)) = ((1, ((a, 0), T)), 0)
+  | unrecognized (Var v) = ((1, v), 1)
+  | unrecognized (Bound i) = ((1, (("", i), dummyT)), 2)
+  | unrecognized (Abs (_, T, _)) = ((1, (("", 0), T)), 3);
+
+fun dest_hd f_ord t =
+      let val ord = f_ord t in
+        if ord = ~1 then unrecognized t else ((0, (("", ord), fastype_of t)), 0)
       end
-  | dest_hd _ (Free (a, T)) = ((1, ((a, 0), T)), 0)
-  | dest_hd _ (Var v) = ((1, v), 1)
-  | dest_hd _ (Bound i) = ((1, (("", i), dummyT)), 2)
-  | dest_hd _ (Abs (_, T, _)) = ((1, (("", 0), T)), 3);
 
 fun term_lpo f_ord (s, t) =
   let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in