--- a/IntEx.thy	Mon Oct 26 14:16:32 2009 +0100
+++ b/IntEx.thy	Mon Oct 26 14:18:26 2009 +0100
@@ -23,6 +23,13 @@
 term ZERO
 thm ZERO_def
 
+(*
+quotient_def (with my_int)
+  ZERO :: "my_int"
+where
+  "ZERO \<equiv> (0::nat, 0::nat)"
+*)
+
 local_setup {*
   make_const_def @{binding ONE} @{term "(1::nat, 0::nat)"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd
 *}

--- a/QuotMain.thy	Mon Oct 26 14:16:32 2009 +0100
+++ b/QuotMain.thy	Mon Oct 26 14:18:26 2009 +0100
@@ -144,8 +144,6 @@
 
 section {* type definition for the quotient type *}
 
-ML {* Toplevel.theory *}
-
 use "quotient.ML"
 
 declare [[map list = (map, LIST_REL)]]
@@ -157,6 +155,25 @@
 ML {* maps_lookup @{theory} "fun" *}
 
 ML {*
+val quot_def_parser = 
+  (OuterParse.$$$ "(" |-- OuterParse.$$$ "with" |-- 
+    ((OuterParse.list1 OuterParse.binding) --| OuterParse.$$$ ")")) --
+      (OuterParse.binding -- 
+        Scan.option (OuterParse.$$$ "::" |-- OuterParse.typ) -- 
+         OuterParse.mixfix --| OuterParse.where_ -- SpecParse.spec)
+*}
+
+ML {*
+fun test (qrtys, (((bind, typstr), mx), (attr, prop))) lthy = lthy
+*}
+
+ML {*
+val _ = OuterSyntax.local_theory "quotient_def" "lifted definition"
+  OuterKeyword.thy_decl (quot_def_parser >> test)
+*}
+
+(* FIXME: auxiliary function *)
+ML {*
 val no_vars = Thm.rule_attribute (fn context => fn th =>
   let
     val ctxt = Variable.set_body false (Context.proof_of context);