diff -r 5f3b364d4765 -r c18308f60f0e QuotMain.thy
--- a/QuotMain.thy	Tue Nov 03 14:04:21 2009 +0100
+++ b/QuotMain.thy	Tue Nov 03 14:04:45 2009 +0100
@@ -1,8 +1,11 @@
 theory QuotMain
 imports QuotScript QuotList Prove
-uses ("quotient.ML")
+uses ("quotient_info.ML") 
+     ("quotient.ML")
 begin
 
+ML {* Attrib.empty_binding *}
+
 locale QUOT_TYPE =
   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
@@ -137,6 +140,7 @@
 
 section {* type definition for the quotient type *}
 
+use "quotient_info.ML"
 use "quotient.ML"
 
 declare [[map list = (map, LIST_REL)]]
@@ -300,11 +304,11 @@
 fun build_qenv lthy qtys = 
 let
   val qenv = map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) (quotdata_lookup lthy)
-  val tsig = Sign.tsig_of (ProofContext.theory_of lthy)
+  val thy = ProofContext.theory_of lthy
   
   fun find_assoc ((qty', rty')::rest) qty =
         let 
-          val inst = Type.typ_match tsig (qty', qty) Vartab.empty
+          val inst = Sign.typ_match thy (qty', qty) Vartab.empty
         in
            (Envir.norm_type inst qty, Envir.norm_type inst rty')
         end
@@ -319,32 +323,40 @@
 end
 *}
 
+
 ML {*
-val qd_parser = 
-  (Args.parens (OuterParse.$$$ "for" |-- (Scan.repeat OuterParse.typ))) --
-    (SpecParse.constdecl -- (SpecParse.opt_thm_name ":" -- OuterParse.prop))
+fun quotdef_cmd qenv ((bind, qty_, mx), (attr, prop)) lthy =
+let    
+  val (lhs_, rhs) = Logic.dest_equals prop
+in
+  make_const_def bind rhs mx qenv lthy
+end
 *}
 
 ML {*
-fun parse_qd_spec (qtystrs, ((bind, tystr, mx), (attr__, propstr))) lthy = 
+val quotdef_parser = 
+  Scan.option (Args.parens (OuterParse.$$$ "for" |-- (Scan.repeat OuterParse.typ))) --
+    (SpecParse.constdecl -- (SpecParse.opt_thm_name ":" -- 
+       OuterParse.prop)) >> OuterParse.triple2
+*}
+
+ML {*
+fun quotdef (qtystrs, (bind, tystr, mx), (attr, propstr)) lthy = 
 let
-  val qtys = map (Syntax.check_typ lthy o Syntax.parse_typ lthy) qtystrs
+  val qtys = map (Syntax.check_typ lthy o Syntax.parse_typ lthy) (the qtystrs)
   val qenv = build_qenv lthy qtys
-  val qty = Syntax.parse_typ lthy (the tystr) |> Syntax.check_typ lthy
+  val qty  = Option.map (Syntax.check_typ lthy o Syntax.parse_typ lthy) tystr
   val prop = Syntax.parse_prop lthy propstr |> Syntax.check_prop lthy
-  val (lhs, rhs) = Logic.dest_equals prop
 in
-  make_const_def bind rhs mx qenv lthy |> snd
+  quotdef_cmd qenv ((bind, qty, mx), (attr, prop)) lthy |> snd
 end
 *}
 
 ML {*
 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"
-  OuterKeyword.thy_decl (qd_parser >> parse_qd_spec)
+  OuterKeyword.thy_decl (quotdef_parser >> quotdef)
 *}
 
-(* ML {* show_all_types := true *} *)
-
 section {* ATOMIZE *}
 
 text {*