# 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;