# HG changeset patch
# User wenzelm
# Date 1305233181 -7200
# Node ID 6c999448c2bbfd3ef02f60f146657ef3a570c4fd
# Parent  29042b3e7575922d0ad8afd93326049c2f2d7374
prefer plain simpset operations;

diff -r 29042b3e7575 -r 6c999448c2bb src/HOL/Tools/Function/lexicographic_order.ML
--- 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
 
diff -r 29042b3e7575 -r 6c999448c2bb src/HOL/Tools/Function/scnp_reconstruct.ML
--- 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