# HG changeset patch
# User krauss
# Date 1193243406 -7200
# Node ID b1ea9d2e6a72bfb890c2557ef17d6b04c1024f1d
# Parent  2650a4a6ad3e755c6a60f3f0eb61e2bae5706c6d
fun command: use "reinit" between "function" and "termination"

diff -r 2650a4a6ad3e -r b1ea9d2e6a72 src/HOL/Tools/function_package/fundef_datatype.ML
--- 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 _ =
diff -r 2650a4a6ad3e -r b1ea9d2e6a72 src/HOL/Tools/function_package/fundef_package.ML
--- 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 *)