src/HOL/Tools/function_package/scnp_reconstruct.ML
changeset 30510 4120fc59dd85
parent 30450 7655e6533209
child 30607 c3d1590debd8
     1.1 --- a/src/HOL/Tools/function_package/scnp_reconstruct.ML	Fri Mar 13 19:53:09 2009 +0100
     1.2 +++ b/src/HOL/Tools/function_package/scnp_reconstruct.ML	Fri Mar 13 19:58:26 2009 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5    val sizechange_tac : Proof.context -> tactic -> tactic
     1.6  
     1.7 -  val decomp_scnp : ScnpSolve.label list -> Proof.context -> method
     1.8 +  val decomp_scnp : ScnpSolve.label list -> Proof.context -> Proof.method
     1.9  
    1.10    val setup : theory -> theory
    1.11  
    1.12 @@ -408,7 +408,7 @@
    1.13      val extra_simps = FundefCommon.TerminationSimps.get ctxt
    1.14      val autom_tac = auto_tac (local_clasimpset_of ctxt addsimps2 extra_simps)
    1.15    in
    1.16 -    Method.SIMPLE_METHOD
    1.17 +    SIMPLE_METHOD
    1.18        (gen_sizechange_tac orders autom_tac ctxt (print_error ctxt))
    1.19    end
    1.20