print the defined constants when finished; tuned
authorkrauss
Fri Oct 26 16:12:58 2007 +0200 (2007-10-26)
changeset 25201e6fe58b640ce
parent 25200 f1d2e106f2fe
child 25202 3a539d9995fb
print the defined constants when finished; tuned
src/HOL/Tools/function_package/fundef_common.ML
src/HOL/Tools/function_package/fundef_package.ML
     1.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Fri Oct 26 15:42:23 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Fri Oct 26 16:12:58 2007 +0200
     1.3 @@ -61,7 +61,7 @@
     1.4        termination: thm
     1.5       }
     1.6  
     1.7 -fun morph_fundef_data phi (FundefCtxData {add_simps, fs, R, psimps, pinducts, termination, defname}) =
     1.8 +fun morph_fundef_data (FundefCtxData {add_simps, fs, R, psimps, pinducts, termination, defname}) phi =
     1.9      let
    1.10        val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
    1.11        val name = Morphism.name phi
    1.12 @@ -98,8 +98,8 @@
    1.13        val ct = cterm_of thy t
    1.14        val inst_morph = lift_morphism thy o Thm.instantiate 
    1.15  
    1.16 -      fun match data = 
    1.17 -          SOME (morph_fundef_data (inst_morph (Thm.match (cterm_of thy (fst data), ct))) (snd data))
    1.18 +      fun match (trm, data) = 
    1.19 +          SOME (morph_fundef_data data (inst_morph (Thm.match (cterm_of thy trm, ct))))
    1.20            handle Pattern.MATCH => NONE
    1.21      in 
    1.22        get_first match (NetRules.retrieve (FundefData.get ctxt) t)
     2.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Fri Oct 26 15:42:23 2007 +0200
     2.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Fri Oct 26 16:12:58 2007 +0200
     2.3 @@ -80,9 +80,10 @@
     2.4  
     2.5        val cdata = FundefCtxData { add_simps=addsmps, psimps=psimps',
     2.6                                    pinducts=snd pinducts', termination=termination', fs=fs, R=R, defname=defname }
     2.7 +      val _ = Specification.print_consts lthy (K false) (map fst fixes)
     2.8      in
     2.9        lthy 
    2.10 -        |> LocalTheory.declaration (fn phi => add_fundef_data (morph_fundef_data phi cdata))
    2.11 +        |> LocalTheory.declaration (add_fundef_data o morph_fundef_data cdata)
    2.12      end (* FIXME: Add cases for induct and cases thm *)
    2.13  
    2.14