--- a/src/HOL/Algebra/ringsimp.ML Thu Nov 24 20:45:34 2011 +0100
+++ b/src/HOL/Algebra/ringsimp.ML Thu Nov 24 21:01:06 2011 +0100
@@ -47,7 +47,7 @@
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) = (Term_Ord.term_lpo ord (a, b) = LESS);
- in asm_full_simp_tac (HOL_ss settermless less addsimps simps) end;
+ in asm_full_simp_tac (HOL_ss addsimps simps |> Simplifier.set_termless less) end;
fun algebra_tac ctxt =
EVERY' (map (fn s => TRY o struct_tac s) (Data.get (Context.Proof ctxt)));