# HG changeset patch
# User wenzelm
# Date 1176504377 -7200
# Node ID cbfb899dd674e6d6b75b26d7fa510b4148154f80
# Parent  2d4d02efd9d95212157a2a78e3264faeb40edca1
data declaration: removed obsolete target_morphism;

diff -r 2d4d02efd9d9 -r cbfb899dd674 src/HOL/Tools/inductive_package.ML
--- 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;