data declaration: removed obsolete target_morphism;

--- a/src/HOL/Tools/inductive_package.ML	Fri Apr 13 21:38:29 2007 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Sat Apr 14 00:46:17 2007 +0200
@@ -725,14 +725,13 @@
        elims = elims',
        raw_induct = rulify raw_induct,
        induct = induct'};
-    val target_result = morph_result (LocalTheory.target_morphism ctxt4) result;
 
     val ctxt5 = ctxt4
       |> Context.proof_map (put_inductives names ({names = names, coind = coind}, result))
       |> LocalTheory.declaration (fn phi =>
         let
           val names' = map (LocalTheory.target_name ctxt4 o Morphism.name phi) names;
-          val result' = morph_result phi target_result;
+          val result' = morph_result phi result;
         in put_inductives names' ({names = names', coind = coind}, result') end);
   in (result, ctxt5) end;