# HG changeset patch
# User krauss
# Date 1272463997 -7200
# Node ID e80a95279ef63ff40f3babd28ca131dd3c033750
# Parent  73ed9f18fdd3d2602aebfa9eb339d71b968b5eb1
return info record (relative to auxiliary context!)

diff -r 73ed9f18fdd3 -r e80a95279ef6 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Wed Apr 28 11:52:04 2010 +0200
+++ b/src/HOL/Tools/Function/function.ML	Wed Apr 28 16:13:17 2010 +0200
@@ -11,11 +11,11 @@
 
   val add_function: (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> Function_Common.function_config ->
-    (Proof.context -> tactic) -> local_theory -> local_theory
+    (Proof.context -> tactic) -> local_theory -> info * local_theory
 
   val add_function_cmd: (binding * string option * mixfix) list ->
     (Attrib.binding * string) list -> Function_Common.function_config ->
-    (Proof.context -> tactic) -> local_theory -> local_theory
+    (Proof.context -> tactic) -> local_theory -> info * local_theory
 
   val function: (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> Function_Common.function_config ->
@@ -126,8 +126,8 @@
           if not is_external then ()
           else Specification.print_consts lthy (K false) (map fst fixes)
       in
-        lthy
-        |> Local_Theory.declaration false (add_function_data o morph_function_data info)
+        (info, 
+         lthy |> Local_Theory.declaration false (add_function_data o morph_function_data info))
       end
   in
     ((goal_state, afterqed), lthy')
@@ -156,7 +156,7 @@
       prepare_function is_external prep default_constraint fixspec eqns config lthy
   in
     lthy'
-    |> Proof.theorem NONE afterqed [[(Logic.unprotect (concl_of goal_state), [])]]
+    |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (concl_of goal_state), [])]]
     |> Proof.refine (Method.primitive_text (K goal_state)) |> Seq.hd
   end