src/HOL/Tools/function_package/fundef_package.ML
changeset 25201 e6fe58b640ce
parent 25169 b1ea9d2e6a72
child 25222 78943ac46f6d
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Fri Oct 26 15:42:23 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Fri Oct 26 16:12:58 2007 +0200
     1.3 @@ -80,9 +80,10 @@
     1.4  
     1.5        val cdata = FundefCtxData { add_simps=addsmps, psimps=psimps',
     1.6                                    pinducts=snd pinducts', termination=termination', fs=fs, R=R, defname=defname }
     1.7 +      val _ = Specification.print_consts lthy (K false) (map fst fixes)
     1.8      in
     1.9        lthy 
    1.10 -        |> LocalTheory.declaration (fn phi => add_fundef_data (morph_fundef_data phi cdata))
    1.11 +        |> LocalTheory.declaration (add_fundef_data o morph_fundef_data cdata)
    1.12      end (* FIXME: Add cases for induct and cases thm *)
    1.13  
    1.14