# HG changeset patch
# User wenzelm
# Date 1331411159 -3600
# Node ID fe8d6532e1c152ef644b345049cc8feeed3ba9b9
# Parent  79f712a9a81535a94388f237a7e0f8bb9b95390a
clarified total_ident_ord, swapping first argument back to normal (unlike e464f84f3680) -- NB: "fast" ord is erratic anyway;

diff -r 79f712a9a815 -r fe8d6532e1c1 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sat Mar 10 20:58:40 2012 +0100
+++ b/src/Pure/Isar/locale.ML	Sat Mar 10 21:25:59 2012 +0100
@@ -244,12 +244,6 @@
 fun ident_le thy ((n: string, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
   (* smaller term is more general *)
 
-(* total order *)
-fun ident_ord ((n: string, ts), (m, ss)) =
-  (case fast_string_ord (m, n) of
-    EQUAL => list_ord Term_Ord.fast_term_ord (ts, ss)
-  | ord => ord);
-
 local
 
 datatype 'a delayed = Ready of 'a | ToDo of 'a delayed * 'a delayed;
@@ -332,7 +326,9 @@
 
 (*** Registrations: interpretations in theories or proof contexts ***)
 
-structure Idtab = Table(type key = string * term list val ord = ident_ord);
+val total_ident_ord = prod_ord fast_string_ord (list_ord Term_Ord.fast_term_ord);
+
+structure Idtab = Table(type key = string * term list val ord = total_ident_ord);
 
 structure Registrations = Generic_Data
 (
@@ -525,7 +521,7 @@
     val deps = dependencies_of thy loc;
   in
     case AList.lookup (fn ((name, morph), ((name', (morph', _)), _)) =>
-      ident_ord ((name, instance_of thy name morph), (name', instance_of thy name' morph')) = EQUAL) deps (name, morph) of
+      total_ident_ord ((name, instance_of thy name morph), (name', instance_of thy name' morph')) = EQUAL) deps (name, morph) of
         NONE => error ("Locale " ^
           quote (extern thy name) ^ " with\parameter instantiation " ^
           space_implode " " (map (quote o Syntax.string_of_term_global thy) morph) ^