# HG changeset patch
# User krauss
# Date 1272628059 -7200
# Node ID 2a9d0ec8c10d1d087f3c2488434bef4e6a3d3d23
# Parent  8da6846b87d9b49ed24f96fac0d9e3389ad504f2
return updated info record after termination proof

diff -r 8da6846b87d9 -r 2a9d0ec8c10d src/HOL/Tools/Function/fun.ML
--- a/src/HOL/Tools/Function/fun.ML	Thu Apr 29 23:55:43 2010 +0200
+++ b/src/HOL/Tools/Function/fun.ML	Fri Apr 30 13:47:39 2010 +0200
@@ -151,7 +151,7 @@
     lthy
     |> add fixes statements config pat_completeness_auto |> snd
     |> Local_Theory.restore
-    |> prove_termination
+    |> prove_termination |> snd
   end
 
 val add_fun = gen_add_fun Function.add_function
diff -r 8da6846b87d9 -r 2a9d0ec8c10d src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Thu Apr 29 23:55:43 2010 +0200
+++ b/src/HOL/Tools/Function/function.ML	Fri Apr 30 13:47:39 2010 +0200
@@ -25,8 +25,10 @@
     (Attrib.binding * string) list -> Function_Common.function_config ->
     local_theory -> Proof.state
 
-  val prove_termination: term option -> tactic -> local_theory -> local_theory
-  val prove_termination_cmd: string option -> tactic -> local_theory -> local_theory
+  val prove_termination: term option -> tactic -> local_theory -> 
+    info * local_theory
+  val prove_termination_cmd: string option -> tactic -> local_theory ->
+    info * local_theory
 
   val termination : term option -> local_theory -> Proof.state
   val termination_cmd : string option -> local_theory -> Proof.state
@@ -195,13 +197,15 @@
              ((qualify "induct",
                [Attrib.internal (K (Rule_Cases.case_names case_names))]),
               tinduct)
-          |-> (fn (simps, (_, inducts)) =>
+          |-> (fn (simps, (_, inducts)) => fn lthy =>
             let val info' = { is_partial=false, defname=defname, add_simps=add_simps,
               case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts,
               simps=SOME simps, inducts=SOME inducts, termination=termination }
             in
-              Local_Theory.declaration false (add_function_data o morph_function_data info')
-              #> Spec_Rules.add Spec_Rules.Equational (fs, tsimps)
+              (info',
+               lthy 
+               |> Local_Theory.declaration false (add_function_data o morph_function_data info')
+               |> Spec_Rules.add Spec_Rules.Equational (fs, tsimps))
             end)
         end
   in
@@ -233,7 +237,7 @@
     |> ProofContext.note_thmss ""
        [((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]),
          [([Goal.norm_result termination], [])])] |> snd
-    |> Proof.theorem NONE afterqed [[(goal, [])]]
+    |> Proof.theorem NONE (snd oo afterqed) [[(goal, [])]]
   end
 
 val termination = gen_termination Syntax.check_term