--- 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 *)
--- a/src/HOL/Tools/inductive_package.ML Thu Nov 23 18:49:55 2006 +0100
+++ b/src/HOL/Tools/inductive_package.ML Thu Nov 23 20:33:25 2006 +0100
@@ -704,8 +704,8 @@
induct = induct'}
in
- (result, LocalTheory.declaration
- (put_inductives cnames ({names = cnames, coind = coind}, result)) ctxt4)
+ (result, LocalTheory.declaration (fn phi => (* FIXME *)
+ (put_inductives cnames ({names = cnames, coind = coind}, result))) ctxt4)
end;