--- a/src/HOL/Algebra/ringsimp.ML Thu Feb 01 15:12:57 2018 +0100
+++ b/src/HOL/Algebra/ringsimp.ML Thu Feb 01 15:31:25 2018 +0100
@@ -47,8 +47,10 @@
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;
- val less = is_less o Term_Ord.term_lpo ord;
- in asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps simps |> Simplifier.set_termless less) end;
+ in
+ asm_full_simp_tac
+ (put_simpset HOL_ss ctxt addsimps simps |> Simplifier.set_term_ord (Term_Ord.term_lpo ord))
+ end;
fun algebra_tac ctxt =
EVERY' (map (fn s => TRY o struct_tac ctxt s) (Data.get (Context.Proof ctxt)));