fixes smlnj-related problem, updated signature
authorkrauss
Tue Jan 23 20:29:03 2007 +0100 (2007-01-23)
changeset 221705682eeaefaf4
parent 22169 74b61ce6b54d
child 22171 58f554f51f0d
fixes smlnj-related problem, updated signature
src/HOL/Tools/function_package/fundef_package.ML
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Jan 23 15:54:22 2007 +0100
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Jan 23 20:29:03 2007 +0100
     1.3 @@ -10,14 +10,14 @@
     1.4  signature FUNDEF_PACKAGE =
     1.5  sig
     1.6      val add_fundef :  (string * string option * mixfix) list
     1.7 -                      -> ((bstring * Attrib.src list) * string list) list list
     1.8 +                      -> ((bstring * Attrib.src list) * (string * bool) list) list list
     1.9                        -> FundefCommon.fundef_config
    1.10                        -> local_theory
    1.11                        -> string * Proof.state
    1.12  
    1.13      val add_fundef_i:  (string * typ option * mixfix) list
    1.14 -                       -> ((bstring * Attrib.src list) * term list) list list
    1.15 -                       -> bool
    1.16 +                       -> ((bstring * Attrib.src list) * (term * bool) list) list list
    1.17 +                       -> FundefCommon.fundef_config
    1.18                         -> local_theory
    1.19                         -> string * Proof.state
    1.20  
    1.21 @@ -32,7 +32,7 @@
    1.22  end
    1.23  
    1.24  
    1.25 -structure FundefPackage  =
    1.26 +structure FundefPackage : FUNDEF_PACKAGE =
    1.27  struct
    1.28  
    1.29  open FundefLib
    1.30 @@ -75,19 +75,19 @@
    1.31            cont (Goal.close_result proof)
    1.32  
    1.33        val qualify = NameSpace.qualified defname
    1.34 -      val addsimps = add_simps fixes spec sort_cont
    1.35 +      val addsmps = add_simps fixes spec sort_cont
    1.36  
    1.37        val (((psimps', pinducts'), (_, [termination'])), lthy) =
    1.38            lthy
    1.39 -            |> addsimps "psimps" [] psimps
    1.40 -            ||> fold_option (snd oo addsimps "simps" []) trsimps
    1.41 +            |> addsmps "psimps" [] psimps
    1.42 +            ||> fold_option (snd oo addsmps "simps" []) trsimps
    1.43              ||>> note_theorem ((qualify "pinduct",
    1.44                                  [Attrib.internal (K (InductAttrib.induct_set ""))]), simple_pinducts)
    1.45              ||>> note_theorem ((qualify "termination", []), [termination])
    1.46              ||> (snd o note_theorem ((qualify "cases", []), [cases]))
    1.47              ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros
    1.48  
    1.49 -      val cdata = FundefCtxData { add_simps=addsimps, psimps=psimps',
    1.50 +      val cdata = FundefCtxData { add_simps=addsmps, psimps=psimps',
    1.51                                    pinducts=snd pinducts', termination=termination', f=f, R=R }
    1.52      in
    1.53        lthy  (* FIXME proper handling of morphism *)