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