merged

--- a/src/HOL/Tools/Function/fun.ML	Wed Dec 29 21:21:11 2010 +0100
+++ b/src/HOL/Tools/Function/fun.ML	Wed Dec 29 22:51:33 2010 +0100
@@ -136,7 +136,7 @@
   Context.theory_map (Function_Common.set_preproc sequential_preproc)
 
 
-val fun_config = FunctionConfig { sequential=true, default="%x. undefined" (*FIXME dynamic scoping*), 
+val fun_config = FunctionConfig { sequential=true, default=NONE,
   domintros=false, partials=false, tailrec=false }
 
 fun gen_add_fun add fixes statements config lthy =

--- a/src/HOL/Tools/Function/function.ML	Wed Dec 29 21:21:11 2010 +0100
+++ b/src/HOL/Tools/Function/function.ML	Wed Dec 29 22:51:33 2010 +0100
@@ -85,11 +85,15 @@
     val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec
 
     val defname = mk_defname fixes
-    val FunctionConfig {partials, tailrec, ...} = config
+    val FunctionConfig {partials, tailrec, default, ...} = config
     val _ =
       if tailrec then Output.legacy_feature
         "'function (tailrec)' command. Use 'partial_function (tailrec)'."
       else ()
+    val _ =
+      if is_some default then Output.legacy_feature
+        "'function (default)'. Use 'partial_function'."
+      else ()
 
     val ((goal_state, cont), lthy') =
       Function_Mutual.prepare_function_mutual config defname fixes eqs lthy

--- a/src/HOL/Tools/Function/function_common.ML	Wed Dec 29 21:21:11 2010 +0100
+++ b/src/HOL/Tools/Function/function_common.ML	Wed Dec 29 22:51:33 2010 +0100
@@ -191,7 +191,7 @@
 
 datatype function_config = FunctionConfig of
  {sequential: bool,
-  default: string,
+  default: string option,
   domintros: bool,
   partials: bool,
   tailrec: bool}
@@ -199,7 +199,7 @@
 fun apply_opt Sequential (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
     FunctionConfig {sequential=true, default=default, domintros=domintros, partials=partials, tailrec=tailrec}
   | apply_opt (Default d) (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
-    FunctionConfig {sequential=sequential, default=d, domintros=domintros, partials=partials, tailrec=tailrec}
+    FunctionConfig {sequential=sequential, default=SOME d, domintros=domintros, partials=partials, tailrec=tailrec}
   | apply_opt DomIntros (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
     FunctionConfig {sequential=sequential, default=default, domintros=true, partials=partials, tailrec=tailrec}
   | apply_opt Tailrec (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
@@ -208,7 +208,7 @@
     FunctionConfig {sequential=sequential, default=default, domintros=domintros, partials=false, tailrec=true}
 
 val default_config =
-  FunctionConfig { sequential=false, default="%x. undefined" (*FIXME dynamic scoping*), 
+  FunctionConfig { sequential=false, default=NONE,
     domintros=false, partials=true, tailrec=false }
 
 

--- a/src/HOL/Tools/Function/function_core.ML	Wed Dec 29 21:21:11 2010 +0100
+++ b/src/HOL/Tools/Function/function_core.ML	Wed Dec 29 22:51:33 2010 +0100
@@ -871,8 +871,9 @@
 
 fun prepare_function config defname [((fname, fT), mixfix)] abstract_qglrs lthy =
   let
-    val FunctionConfig {domintros, tailrec, default=default_str, ...} = config
+    val FunctionConfig {domintros, tailrec, default=default_opt, ...} = config
 
+    val default_str = the_default "%x. undefined" default_opt (*FIXME dynamic scoping*)
     val fvar = Free (fname, fT)
     val domT = domain_type fT
     val ranT = range_type fT

--- a/src/HOL/Tools/Function/induction_schema.ML	Wed Dec 29 21:21:11 2010 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML	Wed Dec 29 22:51:33 2010 +0100
@@ -71,7 +71,7 @@
       end
 
     val (branches, cases') = (* correction *)
-      case Logic.dest_conjunction_list concl of
+      case Logic.dest_conjunctions concl of
         [conc] =>
         let
           val _ $ Pxs = Logic.strip_assums_concl conc