# HG changeset patch
# User krauss
# Date 1154707305 -7200
# Node ID ecdfc96cf4d0844e6d2e7dbb7ac7efde994846d3
# Parent  36e2fae2c68a6d195fa8fbfd066811063e391dba
Added Keywords: "otherwise" and "sequential", needed for function package's
sequential mode.

diff -r 36e2fae2c68a -r ecdfc96cf4d0 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Fri Aug 04 12:01:31 2006 +0200
+++ b/etc/isar-keywords.el	Fri Aug 04 18:01:45 2006 +0200
@@ -259,6 +259,7 @@
     "notes"
     "obtains"
     "open"
+    "otherwise"
     "output"
     "outputs"
     "overloaded"
@@ -267,6 +268,7 @@
     "pre"
     "rename"
     "restrict"
+    "sequential"
     "shows"
     "signature"
     "states"
diff -r 36e2fae2c68a -r ecdfc96cf4d0 src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Fri Aug 04 12:01:31 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Fri Aug 04 18:01:45 2006 +0200
@@ -85,11 +85,6 @@
       val spec = map prep_eqns eqns_attss
       val t_eqnss = map (flat o map snd) spec
 
-(*
- val t_eqns = if preprocess then map (FundefSplit.split_all_equations (ProofContext.init thy)) t_eqns
-              else t_eqns
-*)
-
       val congs = get_fundef_congs (Context.Theory thy)
 
       val (mutual_info, name, (data, thy)) = FundefMutual.prepare_fundef_mutual congs t_eqnss thy
@@ -218,16 +213,16 @@
 
 val opt_attribs_with_star = Scan.optional attribs_with_star ([], false);
 
-fun opt_thm_name_star s =
-  Scan.optional ((P.name -- opt_attribs_with_star || (attribs_with_star >> pair "")) --| P.$$$ s) ("", ([], false));
+val opt_thm_name_star =
+  Scan.optional ((P.name -- opt_attribs_with_star || (attribs_with_star >> pair "")) --| P.$$$ ":") ("", ([], false));
 
 
 val function_decl =
-    Scan.repeat1 (opt_thm_name_star ":" -- P.prop);
+    Scan.repeat1 (opt_thm_name_star -- P.prop);
 
 val functionP =
   OuterSyntax.command "function" "define general recursive functions" K.thy_goal
-  (((Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "pre" -- P.$$$ ")") >> K true) false) --    
+  (((Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "sequential" -- P.$$$ ")") >> K true) false) --    
   P.and_list1 function_decl) >> (fn (prepr, eqnss) =>
                                     Toplevel.print o Toplevel.theory_to_proof (add_fundef eqnss prepr)));
 
@@ -237,6 +232,8 @@
        >> (fn (name,dom) =>
 	      Toplevel.print o Toplevel.theory_to_proof (fundef_setup_termination_proof name dom)));
 
+val _ = OuterSyntax.add_keywords ["sequential", "otherwise"];
+
 val _ = OuterSyntax.add_parsers [functionP];
 val _ = OuterSyntax.add_parsers [terminationP];
 
diff -r 36e2fae2c68a -r ecdfc96cf4d0 src/HOL/Tools/function_package/pattern_split.ML
--- a/src/HOL/Tools/function_package/pattern_split.ML	Fri Aug 04 12:01:31 2006 +0200
+++ b/src/HOL/Tools/function_package/pattern_split.ML	Fri Aug 04 18:01:45 2006 +0200
@@ -103,14 +103,13 @@
 end
 
 
-
 fun split_some_equations ctx eqns =
     let
-      fun split_aux prevs [] = []
+      fun split_aux prev [] = []
         | split_aux prev (((n, (att, true)), eq) :: es) = ((n, att), pattern_subtract_many ctx prev [eq])
                                                           :: split_aux (eq :: prev) es
         | split_aux prev (((n, (att, false)), eq) :: es) = ((n, att), [eq]) 
-                                                                :: split_aux (eq :: prev) es
+                                                           :: split_aux (eq :: prev) es
     in
       split_aux [] eqns
     end