# HG changeset patch
# User krauss
# Date 1272448324 -7200
# Node ID 73ed9f18fdd3d2602aebfa9eb339d71b968b5eb1
# Parent  772ed73e1d619e252e69ae57295b7ad9554db6aa
default termination prover as plain tactic

diff -r 772ed73e1d61 -r 73ed9f18fdd3 src/HOL/FunDef.thy
--- a/src/HOL/FunDef.thy	Wed Apr 28 10:31:15 2010 +0200
+++ b/src/HOL/FunDef.thy	Wed Apr 28 11:52:04 2010 +0200
@@ -314,8 +314,8 @@
 
 ML_val -- "setup inactive"
 {*
-  Context.theory_map (Function_Common.set_termination_prover (ScnpReconstruct.decomp_scnp 
-  [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS])) 
+  Context.theory_map (Function_Common.set_termination_prover
+    (ScnpReconstruct.decomp_scnp_tac [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS]))
 *}
 
 end
diff -r 772ed73e1d61 -r 73ed9f18fdd3 src/HOL/Tools/Function/fun.ML
--- a/src/HOL/Tools/Function/fun.ML	Wed Apr 28 10:31:15 2010 +0200
+++ b/src/HOL/Tools/Function/fun.ML	Wed Apr 28 11:52:04 2010 +0200
@@ -153,7 +153,7 @@
   |> add fixes statements config
   |> by_pat_completeness_auto int
   |> Local_Theory.restore
-  |> termination_by (Function_Common.get_termination_prover lthy) int
+  |> termination_by (SIMPLE_METHOD o Function_Common.get_termination_prover lthy) int
 
 val add_fun = gen_fun Function.function
 val add_fun_cmd = gen_fun Function.function_cmd
diff -r 772ed73e1d61 -r 73ed9f18fdd3 src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Wed Apr 28 10:31:15 2010 +0200
+++ b/src/HOL/Tools/Function/function_common.ML	Wed Apr 28 11:52:04 2010 +0200
@@ -172,7 +172,7 @@
 
 structure TerminationProver = Generic_Data
 (
-  type T = Proof.context -> Proof.method
+  type T = Proof.context -> tactic
   val empty = (fn _ => error "Termination prover not configured")
   val extend = I
   fun merge (a, b) = b  (* FIXME ? *)
diff -r 772ed73e1d61 -r 73ed9f18fdd3 src/HOL/Tools/Function/lexicographic_order.ML
--- a/src/HOL/Tools/Function/lexicographic_order.ML	Wed Apr 28 10:31:15 2010 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Wed Apr 28 11:52:04 2010 +0200
@@ -225,6 +225,6 @@
   Method.setup @{binding lexicographic_order}
     (Method.sections clasimp_modifiers >> (K lexicographic_order))
     "termination prover for lexicographic orderings"
-  #> Context.theory_map (Function_Common.set_termination_prover lexicographic_order)
+  #> Context.theory_map (Function_Common.set_termination_prover (lexicographic_order_tac false))
 
 end;
diff -r 772ed73e1d61 -r 73ed9f18fdd3 src/HOL/Tools/Function/scnp_reconstruct.ML
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Wed Apr 28 10:31:15 2010 +0200
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Wed Apr 28 11:52:04 2010 +0200
@@ -10,7 +10,7 @@
 
   val sizechange_tac : Proof.context -> tactic -> tactic
 
-  val decomp_scnp : ScnpSolve.label list -> Proof.context -> Proof.method
+  val decomp_scnp_tac : ScnpSolve.label list -> Proof.context -> tactic
 
   val setup : theory -> theory
 
@@ -396,13 +396,12 @@
 fun sizechange_tac ctxt autom_tac =
   gen_sizechange_tac [MAX, MS, MIN] autom_tac ctxt (K (K all_tac))
 
-fun decomp_scnp orders ctxt =
+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)
   in
-    SIMPLE_METHOD
-      (gen_sizechange_tac orders autom_tac ctxt (print_error ctxt))
+     gen_sizechange_tac orders autom_tac ctxt (print_error ctxt)
   end
 
 
@@ -416,7 +415,8 @@
   || Scan.succeed [MAX, MS, MIN]
 
 val setup = Method.setup @{binding size_change}
-  (Scan.lift orders --| Method.sections clasimp_modifiers >> decomp_scnp)
+  (Scan.lift orders --| Method.sections clasimp_modifiers >>
+    (fn orders => SIMPLE_METHOD o decomp_scnp_tac orders))
   "termination prover with graph decomposition and the NP subset of size change termination"
 
 end