QuotMain.thy
changeset 205 2a803a1556d5
parent 203 7384115df9fd
child 207 18d7d9dc75cb
child 212 ca9eae5bd871
--- 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)