--- a/QuotMain.thy	Tue Oct 27 14:59:00 2009 +0100
+++ b/QuotMain.thy	Tue Oct 27 15:00:15 2009 +0100
@@ -137,6 +137,8 @@
 
 section {* type definition for the quotient type *}
 
+ML {* Proof.theorem_i NONE *}
+
 use "quotient.ML"
 
 declare [[map list = (map, LIST_REL)]]
@@ -150,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)