# HG changeset patch
# User haftmann
# Date 1196950212 -3600
# Node ID 5c317e8f5673f11924c38936275864903ff8cbe0
# Parent  ea6b11021e79d8e31a871415cb1bfda8a6ecd7b6
dropped void space

diff -r ea6b11021e79 -r 5c317e8f5673 src/HOL/Tools/function_package/fundef_common.ML
--- a/src/HOL/Tools/function_package/fundef_common.ML	Thu Dec 06 15:10:09 2007 +0100
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Thu Dec 06 15:10:12 2007 +0100
@@ -302,7 +302,7 @@
 
 
 local 
-  structure P = OuterParse and K = OuterKeyword 
+  structure P = OuterParse and K = OuterKeyword
 
   val option_parser = (P.reserved "sequential" >> K Sequential)
                    || ((P.reserved "default" |-- P.term) >> Default)