fun command: use "reinit" between "function" and "termination"

--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Wed Oct 24 17:17:43 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Wed Oct 24 18:30:06 2007 +0200
@@ -300,6 +300,7 @@
     lthy
       |> FundefPackage.add_fundef fixes statements config flags
       |> by_pat_completeness_simp
+      |> (fn lthy => LocalTheory.reinit lthy (ProofContext.theory_of lthy))
       |> termination_by_lexicographic_order
 
 val _ =

--- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Oct 24 17:17:43 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Oct 24 18:30:06 2007 +0200
@@ -80,11 +80,9 @@
 
       val cdata = FundefCtxData { add_simps=addsmps, psimps=psimps',
                                   pinducts=snd pinducts', termination=termination', fs=fs, R=R, defname=defname }
-      val cdata' = cdata |> morph_fundef_data (LocalTheory.target_morphism lthy);  (* FIXME !? *)
     in
       lthy 
-        |> LocalTheory.declaration (fn phi => add_fundef_data (morph_fundef_data phi cdata)) (* save in target *)
-        |> Context.proof_map (add_fundef_data cdata') (* also save in local context *)
+        |> LocalTheory.declaration (fn phi => add_fundef_data (morph_fundef_data phi cdata))
     end (* FIXME: Add cases for induct and cases thm *)