--- a/IntEx.thy	Mon Nov 02 15:39:25 2009 +0100
+++ b/IntEx.thy	Mon Nov 02 18:16:19 2009 +0100
@@ -41,6 +41,14 @@
 term PLUS
 thm PLUS_def
 
+definition
+  "MPLUS x y \<equiv> my_plus x y"
+
+term MPLUS
+thm MPLUS_def
+thm MPLUS_def_raw
+
+
 fun
   my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
 where

--- a/QuotMain.thy	Mon Nov 02 15:39:25 2009 +0100
+++ b/QuotMain.thy	Mon Nov 02 18:16:19 2009 +0100
@@ -321,31 +321,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)
 *}
 
-
 section {* ATOMIZE *}
 
 text {*