diff -r 524e0e9cf6b6 -r 2a803a1556d5 QuotMain.thy
--- a/QuotMain.thy	Tue Oct 27 14:15:40 2009 +0100
+++ b/QuotMain.thy	Tue Oct 27 14:46:38 2009 +0100
@@ -152,7 +152,7 @@
 ML {*
 val quot_def_parser = 
   (OuterParse.$$$ "(" |-- OuterParse.$$$ "with" |-- 
-    ((OuterParse.list1 OuterParse.binding) --| OuterParse.$$$ ")")) --
+    ((OuterParse.list1 OuterParse.typ) --| OuterParse.$$$ ")")) --
       (OuterParse.binding -- 
         Scan.option (OuterParse.$$$ "::" |-- OuterParse.typ) -- 
          OuterParse.mixfix --| OuterParse.where_ -- SpecParse.spec)