return updated info record after termination proof
authorkrauss
Fri Apr 30 13:47:39 2010 +0200 (2010-04-30)
changeset 365472a9d0ec8c10d
parent 36544 8da6846b87d9
child 36572 ed99188882b1
child 36577 f412bc3f2454
return updated info record after termination proof
src/HOL/Tools/Function/fun.ML
src/HOL/Tools/Function/function.ML
     1.1 --- a/src/HOL/Tools/Function/fun.ML	Thu Apr 29 23:55:43 2010 +0200
     1.2 +++ b/src/HOL/Tools/Function/fun.ML	Fri Apr 30 13:47:39 2010 +0200
     1.3 @@ -151,7 +151,7 @@
     1.4      lthy
     1.5      |> add fixes statements config pat_completeness_auto |> snd
     1.6      |> Local_Theory.restore
     1.7 -    |> prove_termination
     1.8 +    |> prove_termination |> snd
     1.9    end
    1.10  
    1.11  val add_fun = gen_add_fun Function.add_function
     2.1 --- a/src/HOL/Tools/Function/function.ML	Thu Apr 29 23:55:43 2010 +0200
     2.2 +++ b/src/HOL/Tools/Function/function.ML	Fri Apr 30 13:47:39 2010 +0200
     2.3 @@ -25,8 +25,10 @@
     2.4      (Attrib.binding * string) list -> Function_Common.function_config ->
     2.5      local_theory -> Proof.state
     2.6  
     2.7 -  val prove_termination: term option -> tactic -> local_theory -> local_theory
     2.8 -  val prove_termination_cmd: string option -> tactic -> local_theory -> local_theory
     2.9 +  val prove_termination: term option -> tactic -> local_theory -> 
    2.10 +    info * local_theory
    2.11 +  val prove_termination_cmd: string option -> tactic -> local_theory ->
    2.12 +    info * local_theory
    2.13  
    2.14    val termination : term option -> local_theory -> Proof.state
    2.15    val termination_cmd : string option -> local_theory -> Proof.state
    2.16 @@ -195,13 +197,15 @@
    2.17               ((qualify "induct",
    2.18                 [Attrib.internal (K (Rule_Cases.case_names case_names))]),
    2.19                tinduct)
    2.20 -          |-> (fn (simps, (_, inducts)) =>
    2.21 +          |-> (fn (simps, (_, inducts)) => fn lthy =>
    2.22              let val info' = { is_partial=false, defname=defname, add_simps=add_simps,
    2.23                case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts,
    2.24                simps=SOME simps, inducts=SOME inducts, termination=termination }
    2.25              in
    2.26 -              Local_Theory.declaration false (add_function_data o morph_function_data info')
    2.27 -              #> Spec_Rules.add Spec_Rules.Equational (fs, tsimps)
    2.28 +              (info',
    2.29 +               lthy 
    2.30 +               |> Local_Theory.declaration false (add_function_data o morph_function_data info')
    2.31 +               |> Spec_Rules.add Spec_Rules.Equational (fs, tsimps))
    2.32              end)
    2.33          end
    2.34    in
    2.35 @@ -233,7 +237,7 @@
    2.36      |> ProofContext.note_thmss ""
    2.37         [((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]),
    2.38           [([Goal.norm_result termination], [])])] |> snd
    2.39 -    |> Proof.theorem NONE afterqed [[(goal, [])]]
    2.40 +    |> Proof.theorem NONE (snd oo afterqed) [[(goal, [])]]
    2.41    end
    2.42  
    2.43  val termination = gen_termination Syntax.check_term