src/HOL/Tools/function_package/fundef_package.ML

             ||> (snd o note_theorem ((qualify "cases", []), [cases]))
             ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros
 
       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 *)
 
 
 fun gen_add_fundef prep fixspec eqnss config flags lthy =
     let