# HG changeset patch
# User wenzelm
# Date 1176504378 -7200
# Node ID 8183ee5792328e50810648808d8666e3b2f9f828
# Parent  cbfb899dd674e6d6b75b26d7fa510b4148154f80
data declaration: removed obsolete target_morphism (still required for local data!?);

diff -r cbfb899dd674 -r 8183ee579232 src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Sat Apr 14 00:46:17 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Sat Apr 14 00:46:18 2007 +0200
@@ -88,11 +88,11 @@
 
       val cdata = FundefCtxData { add_simps=addsmps, psimps=psimps',
                                   pinducts=snd pinducts', termination=termination', f=f, R=R }
-            |> morph_fundef_data (LocalTheory.target_morphism lthy)
+      val cdata' = cdata |> morph_fundef_data (LocalTheory.target_morphism lthy);  (* FIXME !? *)
     in
       lthy 
         |> LocalTheory.declaration (fn phi => add_fundef_data defname (morph_fundef_data phi cdata)) (* save in target *)
-        |> Context.proof_map (add_fundef_data defname cdata) (* also save in local context *)
+        |> Context.proof_map (add_fundef_data defname cdata') (* also save in local context *)
     end (* FIXME: Add cases for induct and cases thm *)