diff -r 6aefc5ff8e63 -r 5c25a2012975 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/rule_cases.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Annotations and local contexts of rules.
@@ -319,7 +318,7 @@
 local
 
 fun equal_cterms ts us =
-  is_equal (list_ord (Term.fast_term_ord o pairself Thm.term_of) (ts, us));
+  is_equal (list_ord (TermOrd.fast_term_ord o pairself Thm.term_of) (ts, us));
 
 fun prep_rule n th =
   let