diff -r 74b61ce6b54d -r 5682eeaefaf4 src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Jan 23 15:54:22 2007 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Jan 23 20:29:03 2007 +0100
@@ -10,14 +10,14 @@
 signature FUNDEF_PACKAGE =
 sig
     val add_fundef :  (string * string option * mixfix) list
-                      -> ((bstring * Attrib.src list) * string list) list list
+                      -> ((bstring * Attrib.src list) * (string * bool) list) list list
                       -> FundefCommon.fundef_config
                       -> local_theory
                       -> string * Proof.state
 
     val add_fundef_i:  (string * typ option * mixfix) list
-                       -> ((bstring * Attrib.src list) * term list) list list
-                       -> bool
+                       -> ((bstring * Attrib.src list) * (term * bool) list) list list
+                       -> FundefCommon.fundef_config
                        -> local_theory
                        -> string * Proof.state
 
@@ -32,7 +32,7 @@
 end
 
 
-structure FundefPackage  =
+structure FundefPackage : FUNDEF_PACKAGE =
 struct
 
 open FundefLib
@@ -75,19 +75,19 @@
           cont (Goal.close_result proof)
 
       val qualify = NameSpace.qualified defname
-      val addsimps = add_simps fixes spec sort_cont
+      val addsmps = add_simps fixes spec sort_cont
 
       val (((psimps', pinducts'), (_, [termination'])), lthy) =
           lthy
-            |> addsimps "psimps" [] psimps
-            ||> fold_option (snd oo addsimps "simps" []) trsimps
+            |> addsmps "psimps" [] psimps
+            ||> fold_option (snd oo addsmps "simps" []) trsimps
             ||>> note_theorem ((qualify "pinduct",
                                 [Attrib.internal (K (InductAttrib.induct_set ""))]), simple_pinducts)
             ||>> note_theorem ((qualify "termination", []), [termination])
             ||> (snd o note_theorem ((qualify "cases", []), [cases]))
             ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros
 
-      val cdata = FundefCtxData { add_simps=addsimps, psimps=psimps',
+      val cdata = FundefCtxData { add_simps=addsmps, psimps=psimps',
                                   pinducts=snd pinducts', termination=termination', f=f, R=R }
     in
       lthy  (* FIXME proper handling of morphism *)