src/HOL/Import/shuffler.ML
changeset 29269 5c25a2012975
parent 29265 5b4247055bd7
child 29270 0eade173f77e
     1.1 --- a/src/HOL/Import/shuffler.ML	Wed Dec 31 00:08:14 2008 +0100
     1.2 +++ b/src/HOL/Import/shuffler.ML	Wed Dec 31 15:30:10 2008 +0100
     1.3 @@ -353,7 +353,7 @@
     1.4  
     1.5  fun equals_fun thy assume t =
     1.6      case t of
     1.7 -        Const("op ==",_) $ u $ v => if Term.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE
     1.8 +        Const("op ==",_) $ u $ v => if TermOrd.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE
     1.9        | _ => NONE
    1.10  
    1.11  fun eta_expand thy assumes origt =