print the defined constants when finished; tuned

--- a/src/HOL/Tools/function_package/fundef_common.ML	Fri Oct 26 15:42:23 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Fri Oct 26 16:12:58 2007 +0200
@@ -61,7 +61,7 @@
       termination: thm
      }
 
-fun morph_fundef_data phi (FundefCtxData {add_simps, fs, R, psimps, pinducts, termination, defname}) =
+fun morph_fundef_data (FundefCtxData {add_simps, fs, R, psimps, pinducts, termination, defname}) phi =
     let
       val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
       val name = Morphism.name phi
@@ -98,8 +98,8 @@
       val ct = cterm_of thy t
       val inst_morph = lift_morphism thy o Thm.instantiate 
 
-      fun match data = 
-          SOME (morph_fundef_data (inst_morph (Thm.match (cterm_of thy (fst data), ct))) (snd data))
+      fun match (trm, data) = 
+          SOME (morph_fundef_data data (inst_morph (Thm.match (cterm_of thy trm, ct))))
           handle Pattern.MATCH => NONE
     in 
       get_first match (NetRules.retrieve (FundefData.get ctxt) t)

--- 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 *)