--- a/src/HOL/Tools/function_package/fundef_package.ML Fri Oct 26 15:42:23 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML Fri Oct 26 16:12:58 2007 +0200
@@ -80,9 +80,10 @@
val cdata = FundefCtxData { add_simps=addsmps, psimps=psimps',
pinducts=snd pinducts', termination=termination', fs=fs, R=R, defname=defname }
+ val _ = Specification.print_consts lthy (K false) (map fst fixes)
in
lthy
- |> LocalTheory.declaration (fn phi => add_fundef_data (morph_fundef_data phi cdata))
+ |> LocalTheory.declaration (add_fundef_data o morph_fundef_data cdata)
end (* FIXME: Add cases for induct and cases thm *)