--- a/src/HOL/Algebra/ringsimp.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/HOL/Algebra/ringsimp.ML Sat Feb 27 23:13:01 2010 +0100
@@ -46,7 +46,7 @@
val ops = map (fst o Term.strip_comb) ts;
fun ord (Const (a, _)) = find_index (fn (Const (b, _)) => a=b | _ => false) ops
| ord (Free (a, _)) = find_index (fn (Free (b, _)) => a=b | _ => false) ops;
- fun less (a, b) = (TermOrd.term_lpo ord (a, b) = LESS);
+ fun less (a, b) = (Term_Ord.term_lpo ord (a, b) = LESS);
in asm_full_simp_tac (HOL_ss settermless less addsimps simps) end;
fun algebra_tac ctxt =