--- a/src/HOL/Tools/function_package/fundef_package.ML Thu Nov 23 18:49:55 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML Thu Nov 23 20:33:25 2006 +0100
@@ -88,8 +88,8 @@
in
- lthy
- |> LocalTheory.declaration (add_fundef_data defname cdata) (* save in target *)
+ lthy (* FIXME proper handling of morphism *)
+ |> LocalTheory.declaration (fn phi => add_fundef_data defname 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 *)