--- 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
--- 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
--- 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 ? *)
--- 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;
--- 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