--- a/src/HOL/Tools/function_package/fundef_package.ML Tue Apr 10 14:11:01 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML Tue Apr 10 18:09:58 2007 +0200
@@ -69,6 +69,8 @@
end
+fun pr_ctxdata (x: fundef_context_data) = (Output.debug (K (PolyML.makestring x)); x)
+
fun fundef_afterqed config fixes spec defname cont sort_cont [[proof]] lthy =
let
val FundefResult {f, R, psimps, trsimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} =
@@ -89,9 +91,10 @@
val cdata = FundefCtxData { add_simps=addsmps, psimps=psimps',
pinducts=snd pinducts', termination=termination', f=f, R=R }
+ |> morph_fundef_data (LocalTheory.target_morphism lthy)
in
- lthy (* FIXME proper handling of morphism *)
- |> LocalTheory.declaration (fn phi => add_fundef_data defname cdata) (* save in target *)
+ lthy
+ |> LocalTheory.declaration (fn phi => add_fundef_data defname (pr_ctxdata (morph_fundef_data phi cdata))) (* save in target *)
|> Context.proof_map (add_fundef_data defname cdata) (* also save in local context *)
end (* FIXME: Add cases for induct and cases thm *)