# HG changeset patch
# User krauss
# Date 1238423843 -7200
# Node ID 02aa92682e88091ebc12295f0b3b89db0cf2c6a7
# Parent  350bb108406d15323a00c0165bb11c873c6a208a
use standard parsers provided by SpecParse

diff -r 350bb108406d -r 02aa92682e88 src/HOL/Tools/function_package/fundef_common.ML
--- a/src/HOL/Tools/function_package/fundef_common.ML	Mon Mar 30 16:37:23 2009 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Mon Mar 30 16:37:23 2009 +0200
@@ -344,18 +344,9 @@
   fun config_parser default = 
       (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 option_parser) --| P.$$$ ")") [])
         >> (fn opts => fold apply_opt opts default)
-
-  fun pipe_error t = 
-  P.!!! (Scan.fail_with (K (cat_lines ["Equations must be separated by " ^ quote "|", quote t])))
-
-  val statement = 
-   SpecParse.opt_thm_name ":" -- P.prop
-    --| Scan.ahead ((P.term :-- pipe_error) || Scan.succeed ("",""))
-
-  val statements = P.enum1 "|" statement
 in
   fun fundef_parser default_cfg = 
-      config_parser default_cfg -- P.fixes --| P.where_ -- statements
+      config_parser default_cfg -- P.fixes -- SpecParse.where_alt_specs
 end