diff -r 0370493040f3 -r 5fe163543bb8 quotient.ML
--- a/quotient.ML	Mon Oct 12 13:58:31 2009 +0200
+++ b/quotient.ML	Mon Oct 12 14:30:50 2009 +0200
@@ -162,6 +162,26 @@
       in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)
 end
 
+(* syntax setup *)
+local structure P = OuterParse in
+
+val quottype_parser = 
+    (P.type_args -- P.binding) -- 
+      P.opt_infix -- 
+       (P.$$$ "=" |-- P.term) -- 
+         (P.$$$ "/" |-- P.term)
+           
+(*
+val _ =
+  OuterSyntax.command "quotient" "quotient type definition (requires equivalence proof)"
+    OuterKeyword.thy_goal
+    (typedef_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef)));
+
+end;
+*)
+
+end;
+
 end;
 
 open Quotient
\ No newline at end of file