--- a/src/HOL/Tools/function_package/fundef_core.ML Fri Jun 01 15:20:53 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_core.ML Fri Jun 01 15:57:45 2007 +0200
@@ -10,9 +10,8 @@
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 *)
@@ -858,9 +857,9 @@
end
-fun prepare_fundef config defname (fname, fT, mixfix) abstract_qglrs default_str lthy =
+fun prepare_fundef config defname [((fname, fT), mixfix)] abstract_qglrs lthy =
let
- val FundefConfig {domintros, tailrec, ...} = config
+ val FundefConfig {domintros, tailrec, default=default_str, ...} = config
val fvar = Free (fname, fT)
val domT = domain_type fT