# HG changeset patch
# User krauss
# Date 1272439308 -7200
# Node ID a33b986f2e22d7a2d71fb398a2588559411865db
# Parent  0dcd03d521ec19429e3944cd2083b8ffdc17294d
function: better separate Isar integration from actual functionality

diff -r 0dcd03d521ec -r a33b986f2e22 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Thu Apr 29 07:02:22 2010 +0200
+++ b/src/HOL/Tools/Function/function.ML	Wed Apr 28 09:21:48 2010 +0200
@@ -65,7 +65,7 @@
     (saved_simps, fold2 add_for_f fnames simps_by_f lthy)
   end
 
-fun gen_add_function is_external prep default_constraint fixspec eqns config lthy =
+fun prepare_function is_external prep default_constraint fixspec eqns config lthy =
   let
     val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
     val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy
@@ -118,8 +118,16 @@
         lthy
         |> Local_Theory.declaration false (add_function_data o morph_function_data info)
       end
+  in 
+    ((goalstate, afterqed), lthy)
+  end
+
+fun gen_add_function is_external prep default_constraint fixspec eqns config lthy =
+  let
+    val ((goalstate, afterqed), lthy') = 
+      prepare_function is_external prep default_constraint fixspec eqns config lthy
   in
-    lthy
+    lthy'
     |> Proof.theorem NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
     |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
   end
@@ -128,7 +136,7 @@
   gen_add_function false Specification.check_spec (TypeInfer.anyT HOLogic.typeS)
 val add_function_cmd = gen_add_function true Specification.read_spec "_::type"
                                                 
-fun gen_termination_proof prep_term raw_term_opt lthy =
+fun prepare_termination_proof prep_term raw_term_opt lthy =
   let
     val term_opt = Option.map (prep_term lthy) raw_term_opt
     val info = the (case term_opt of
@@ -169,6 +177,13 @@
             end)
         end
   in
+    (goal, afterqed, termination)
+  end
+
+fun gen_termination_proof prep_term raw_term_opt lthy =
+  let
+    val (goal, afterqed, termination) = prepare_termination_proof prep_term raw_term_opt lthy
+  in
     lthy
     |> ProofContext.note_thmss ""
        [((Binding.empty, [Context_Rules.rule_del]), [([allI], [])])] |> snd