src/Pure/Isar/locale.ML
changeset 29269 5c25a2012975
parent 29004 a5a91f387791
child 29275 9fa69e3858d6
     1.1 --- a/src/Pure/Isar/locale.ML	Wed Dec 31 00:08:14 2008 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Wed Dec 31 15:30:10 2008 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4  (*  Title:      Pure/Isar/locale.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Clemens Ballarin, TU Muenchen; Markus Wenzel, LMU/TU Muenchen
     1.7 +    Author:     Clemens Ballarin, TU Muenchen
     1.8 +    Author:     Markus Wenzel, LMU/TU Muenchen
     1.9  
    1.10  Locales -- Isar proof contexts as meta-level predicates, with local
    1.11  syntax and implicit structures.
    1.12 @@ -1297,7 +1297,7 @@
    1.13  
    1.14  fun defs_ord (defs1, defs2) =
    1.15      list_ord (fn ((_, (d1, _)), (_, (d2, _))) =>
    1.16 -      Term.fast_term_ord (d1, d2)) (defs1, defs2);
    1.17 +      TermOrd.fast_term_ord (d1, d2)) (defs1, defs2);
    1.18  structure Defstab =
    1.19      TableFun(type key = (Attrib.binding * (term * term list)) list val ord = defs_ord);
    1.20