src/HOL/Tools/function_package/fundef_core.ML

 
 signature FUNDEF_CORE =
 sig
     val prepare_fundef : FundefCommon.fundef_config
                          -> string (* defname *)
-                         -> (string * typ * mixfix) (* defined symbol *)
+                         -> ((string * typ) * mixfix) list (* defined symbol *)
                          -> ((string * typ) list * term list * term * term) list (* specification *)
-                         -> string (* default_value, not parsed yet *)
                          -> local_theory
 
                          -> (term   (* f *)
                              * thm  (* goalstate *)
                              * (thm -> FundefCommon.fundef_result) (* continuation *)

     in
       map2 mk_trsimp clauses psimps
     end
 
 
-fun prepare_fundef config defname (fname, fT, mixfix) abstract_qglrs default_str lthy =
-    let
-      val FundefConfig {domintros, tailrec, ...} = config 
+fun prepare_fundef config defname [((fname, fT), mixfix)] abstract_qglrs lthy =
+    let
+      val FundefConfig {domintros, tailrec, default=default_str, ...} = config 
                                                          
       val fvar = Free (fname, fT)
       val domT = domain_type fT
       val ranT = range_type fT