configuration flag "partials"

--- a/src/HOL/Tools/Function/fun.ML	Fri Oct 23 16:37:56 2009 +0200
+++ b/src/HOL/Tools/Function/fun.ML	Sat Oct 24 20:47:10 2009 +0200
@@ -148,7 +148,7 @@
 
 
 val fun_config = FunctionConfig { sequential=true, default="%x. undefined" (*FIXME dynamic scoping*), 
-                                domintros=false, tailrec=false }
+  domintros=false, partials=false, tailrec=false }
 
 fun gen_fun add config fixes statements int lthy =
   let val group = serial_string () in

--- a/src/HOL/Tools/Function/function.ML	Fri Oct 23 16:37:56 2009 +0200
+++ b/src/HOL/Tools/Function/function.ML	Sat Oct 24 20:47:10 2009 +0200
@@ -77,6 +77,7 @@
       val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec
 
       val defname = mk_defname fixes
+      val FunctionConfig {partials, ...} = config
 
       val ((goalstate, cont), lthy) =
           Function_Mutual.prepare_function_mutual config defname fixes eqs lthy

--- a/src/HOL/Tools/Function/function_common.ML	Fri Oct 23 16:37:56 2009 +0200
+++ b/src/HOL/Tools/Function/function_common.ML	Sat Oct 24 20:47:10 2009 +0200
@@ -170,6 +170,7 @@
   = Sequential
   | Default of string
   | DomIntros
+  | No_Partials
   | Tailrec
 
 datatype function_config
@@ -178,21 +179,24 @@
     sequential: bool,
     default: string,
     domintros: bool,
+    partials: bool,
     tailrec: bool
    }
 
-fun apply_opt Sequential (FunctionConfig {sequential, default, domintros,tailrec}) = 
-    FunctionConfig {sequential=true, default=default, domintros=domintros, tailrec=tailrec}
-  | apply_opt (Default d) (FunctionConfig {sequential, default, domintros,tailrec}) = 
-    FunctionConfig {sequential=sequential, default=d, domintros=domintros, tailrec=tailrec}
-  | apply_opt DomIntros (FunctionConfig {sequential, default, domintros,tailrec}) =
-    FunctionConfig {sequential=sequential, default=default, domintros=true,tailrec=tailrec}
-  | apply_opt Tailrec (FunctionConfig {sequential, default, domintros,tailrec}) =
-    FunctionConfig {sequential=sequential, default=default, domintros=domintros,tailrec=true}
+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}
+  | 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}) =
+    FunctionConfig {sequential=sequential, default=default, domintros=domintros, partials=partials, tailrec=true}
+  | apply_opt No_Partials (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
+    FunctionConfig {sequential=sequential, default=default, domintros=domintros, partials=false, tailrec=true}
 
 val default_config =
   FunctionConfig { sequential=false, default="%x. undefined" (*FIXME dynamic scoping*), 
-                 domintros=false, tailrec=false }
+    domintros=false, partials=true, tailrec=false }
 
 
 (* Analyzing function equations *)
@@ -327,6 +331,7 @@
       P.group "option" ((P.reserved "sequential" >> K Sequential)
                     || ((P.reserved "default" |-- P.term) >> Default)
                     || (P.reserved "domintros" >> K DomIntros)
+                    || (P.reserved "no_partials" >> K No_Partials)
                     || (P.reserved "tailrec" >> K Tailrec))
 
   fun config_parser default =