--- a/src/HOL/Tools/Function/lexicographic_order.ML Thu May 12 22:37:31 2011 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Thu May 12 22:46:21 2011 +0200
@@ -216,7 +216,7 @@
fun lexicographic_order_tac quiet ctxt =
TRY (Function_Common.apply_termination_rule ctxt 1)
THEN lex_order_tac quiet ctxt
- (auto_tac (clasimpset_of ctxt addsimps2 Function_Common.Termination_Simps.get ctxt))
+ (auto_tac (claset_of ctxt, simpset_of ctxt addsimps Function_Common.Termination_Simps.get ctxt))
val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac false
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Thu May 12 22:37:31 2011 +0200
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Thu May 12 22:46:21 2011 +0200
@@ -338,7 +338,7 @@
fun decomp_scnp_tac orders ctxt =
let
val extra_simps = Function_Common.Termination_Simps.get ctxt
- val autom_tac = auto_tac (clasimpset_of ctxt addsimps2 extra_simps)
+ val autom_tac = auto_tac (claset_of ctxt, simpset_of ctxt addsimps extra_simps)
in
gen_sizechange_tac orders autom_tac ctxt
end