--- 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);