remove "otherwise" feature from function package which was never really documented or used

--- a/src/HOL/Tools/function_package/fundef_common.ML	Mon Mar 30 12:25:52 2009 +1100
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Mon Mar 30 14:42:36 2009 +0200
@@ -290,7 +290,7 @@
 
 type fixes = ((string * typ) * mixfix) list
 type 'a spec = ((bstring * Attrib.src list) * 'a list) list
-type preproc = fundef_config -> bool list -> Proof.context -> fixes -> term spec 
+type preproc = fundef_config -> Proof.context -> fixes -> term spec 
                -> (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list)
 
 val fname_of = fst o dest_Free o fst o strip_comb o fst 
@@ -301,7 +301,7 @@
   | mk_case_names _ n 1 = [n]
   | mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k)
 
-fun empty_preproc check _ _ ctxt fixes spec =
+fun empty_preproc check _ ctxt fixes spec =
     let 
       val (nas,tss) = split_list spec
       val ts = flat tss
@@ -345,22 +345,17 @@
       (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 option_parser) --| P.$$$ ")") [])
         >> (fn opts => fold apply_opt opts default)
 
-  val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
-
   fun pipe_error t = 
   P.!!! (Scan.fail_with (K (cat_lines ["Equations must be separated by " ^ quote "|", quote t])))
 
-  val statement_ow = 
-   SpecParse.opt_thm_name ":" -- (P.prop -- Scan.optional (otherwise >> K true) false)
+  val statement = 
+   SpecParse.opt_thm_name ":" -- P.prop
     --| Scan.ahead ((P.term :-- pipe_error) || Scan.succeed ("",""))
 
-  val statements_ow = P.enum1 "|" statement_ow
-
-  val flags_statements = statements_ow
-                         >> (fn sow => (map (snd o snd) sow, map (apsnd fst) sow))
+  val statements = P.enum1 "|" statement
 in
   fun fundef_parser default_cfg = 
-      config_parser default_cfg -- P.fixes --| P.where_ -- flags_statements
+      config_parser default_cfg -- P.fixes --| P.where_ -- statements
 end
 
 

--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Mar 30 12:25:52 2009 +1100
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Mar 30 14:42:36 2009 +0200
@@ -15,10 +15,10 @@
 
     val add_fun : FundefCommon.fundef_config ->
       (binding * typ option * mixfix) list -> (Attrib.binding * term) list ->
-      bool list -> bool -> local_theory -> Proof.context
+      bool -> local_theory -> Proof.context
     val add_fun_cmd : FundefCommon.fundef_config ->
       (binding * string option * mixfix) list -> (Attrib.binding * string) list ->
-      bool list -> bool -> local_theory -> Proof.context
+      bool -> local_theory -> Proof.context
 end
 
 structure FundefDatatype : FUNDEF_DATATYPE =
@@ -235,32 +235,23 @@
     end
 
 fun add_catchall ctxt fixes spec =
-    let 
-      val catchalls = mk_catchall fixes (mk_arities (map (split_def ctxt) (map snd spec)))
-    in
-      spec @ map (pair true) catchalls
-    end
+    spec @ mk_catchall fixes (mk_arities (map (split_def ctxt) spec))
 
 fun warn_if_redundant ctxt origs tss =
     let
         fun msg t = "Ignoring redundant equation: " ^ quote (Syntax.string_of_term ctxt t)
                     
         val (tss', _) = chop (length origs) tss
-        fun check ((_, t), []) = (Output.warning (msg t); [])
-          | check ((_, t), s) = s
+        fun check (t, []) = (Output.warning (msg t); [])
+          | check (t, s) = s
     in
         (map check (origs ~~ tss'); tss)
     end
 
 
-fun sequential_preproc (config as FundefConfig {sequential, ...}) flags ctxt fixes spec =
-    let
-      val enabled = sequential orelse exists I flags
-    in 
-      if enabled then
+fun sequential_preproc (config as FundefConfig {sequential, ...}) ctxt fixes spec =
+      if sequential then
         let
-          val flags' = if sequential then map (K true) flags else flags
-
           val (nas, eqss) = split_list spec
                             
           val eqs = map the_single eqss
@@ -268,12 +259,11 @@
           val feqs = eqs
                       |> tap (check_defs ctxt fixes) (* Standard checks *)
                       |> tap (map (check_pats ctxt))    (* More checks for sequential mode *)
-                      |> curry op ~~ flags'
 
           val compleqs = add_catchall ctxt fixes feqs   (* Completion *)
 
           val spliteqs = warn_if_redundant ctxt feqs
-                           (FundefSplit.split_some_equations ctxt compleqs)
+                           (FundefSplit.split_all_equations ctxt compleqs)
 
           fun restore_spec thms =
               nas ~~ Library.take (length nas, Library.unflat spliteqs thms)
@@ -296,8 +286,7 @@
           (flat spliteqs, restore_spec, sort, case_names)
         end
       else
-        FundefCommon.empty_preproc check_defs config flags ctxt fixes spec
-    end
+        FundefCommon.empty_preproc check_defs config ctxt fixes spec
 
 val setup =
     Method.setup @{binding pat_completeness} (Scan.succeed pat_completeness)
@@ -308,11 +297,11 @@
 val fun_config = FundefConfig { sequential=true, default="%x. undefined" (*FIXME dynamic scoping*), 
                                 domintros=false, tailrec=false }
 
-fun gen_fun add config fixes statements flags int lthy =
+fun gen_fun add config fixes statements int lthy =
   let val group = serial_string () in
     lthy
       |> LocalTheory.set_group group
-      |> add fixes statements config flags
+      |> add fixes statements config
       |> by_pat_completeness_auto int
       |> LocalTheory.restore
       |> LocalTheory.set_group group
@@ -329,7 +318,7 @@
 val _ =
   OuterSyntax.local_theory' "fun" "define general recursive functions (short version)" K.thy_decl
   (fundef_parser fun_config
-     >> (fn ((config, fixes), (flags, statements)) => add_fun_cmd config fixes statements flags));
+     >> (fn ((config, fixes), statements) => add_fun_cmd config fixes statements));
 
 end
 

--- a/src/HOL/Tools/function_package/fundef_package.ML	Mon Mar 30 12:25:52 2009 +1100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Mon Mar 30 14:42:36 2009 +0200
@@ -10,13 +10,11 @@
     val add_fundef :  (binding * typ option * mixfix) list
                        -> (Attrib.binding * term) list
                        -> FundefCommon.fundef_config
-                       -> bool list
                        -> local_theory
                        -> Proof.state
     val add_fundef_cmd :  (binding * string option * mixfix) list
                       -> (Attrib.binding * string) list 
                       -> FundefCommon.fundef_config
-                      -> bool list
                       -> local_theory
                       -> Proof.state
 
@@ -95,13 +93,13 @@
     end
 
 
-fun gen_add_fundef is_external prep default_constraint fixspec eqns config flags lthy =
+fun gen_add_fundef is_external prep default_constraint fixspec eqns config lthy =
     let
       val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
       val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy
       val fixes = map (apfst (apfst Binding.name_of)) fixes0;
       val spec = map (fn ((b, atts), prop) => ((Binding.name_of b, atts), [prop])) spec0;
-      val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
+      val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config ctxt' fixes spec
 
       val defname = mk_defname fixes
 
@@ -209,12 +207,10 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
-val _ = OuterKeyword.keyword "otherwise";
-
 val _ =
   OuterSyntax.local_theory_to_proof "function" "define general recursive functions" K.thy_goal
   (fundef_parser default_config
-     >> (fn ((config, fixes), (flags, statements)) => add_fundef_cmd fixes statements config flags));
+     >> (fn ((config, fixes), statements) => add_fundef_cmd fixes statements config));
 
 val _ =
   OuterSyntax.local_theory_to_proof "termination" "prove termination of a recursive function" K.thy_goal