--- a/quotient.ML	Mon Oct 12 22:44:16 2009 +0200
+++ b/quotient.ML	Mon Oct 12 23:06:14 2009 +0200
@@ -1,13 +1,11 @@
-
-
 
 structure Quotient =
 struct
 
-(* constructs the term lambda (c::rty => bool). EX x. c= rel x *)
+(* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *)
 fun typedef_term rel rty lthy =
 let
-  val [x, c] = [("x", rty), ("c", rty --> @{typ bool})]
+  val [x, c] = [("x", rty), ("c", HOLogic.mk_setT rty)]
                |> Variable.variant_frees lthy [rel]
                |> map Free
 in
@@ -80,7 +78,7 @@
 end
 
 (* two wrappers for define and note *)
-fun make_def (name, mx, rhs) lthy =
+fun define (name, mx, rhs) lthy =
 let
   val ((rhs, (_ , thm)), lthy') =
      LocalTheory.define Thm.internalK ((name, mx), (Attrib.empty_binding, rhs)) lthy
@@ -88,7 +86,7 @@
   ((rhs, thm), lthy')
 end
 
-fun note_thm (name, thm) lthy =
+fun note (name, thm) lthy =
 let
   val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy
 in
@@ -117,8 +115,8 @@
   val ABS_name = Binding.prefix_name "ABS_" qty_name
   val REP_name = Binding.prefix_name "REP_" qty_name
   val (((ABS, ABS_def), (REP, REP_def)), lthy2) =
-         lthy1 |> make_def (ABS_name, NoSyn, ABS_trm)
-               ||>> make_def (REP_name, NoSyn, REP_trm)
+         lthy1 |> define (ABS_name, NoSyn, ABS_trm)
+               ||>> define (REP_name, NoSyn, REP_trm)
 
   (* quot_type theorem *)
   val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy2
@@ -151,8 +149,8 @@
     ]))]
 in
   lthy4
-  |> note_thm (quot_thm_name, quot_thm)
-  ||>> note_thm (quotient_thm_name, quotient_thm)
+  |> note (quot_thm_name, quot_thm)
+  ||>> note (quotient_thm_name, quotient_thm)
   ||> LocalTheory.theory (fn thy =>
       let
         val global_eqns = map exp_term [eqn2i, eqn1i];
@@ -165,23 +163,53 @@
 (* syntax setup *)
 local structure P = OuterParse in
 
+fun mk_typedef (qty, mx, rty, rel_trm) lthy = 
+let
+  val (qty_name, _) = Term.dest_Type qty 
+
+  val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
+  val EQUIV_goal = HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel_trm)
+		   
+  val _ = [Syntax.string_of_term lthy EQUIV_goal,
+           Syntax.string_of_typ lthy (fastype_of rel_trm),
+           Syntax.string_of_typ lthy EQUIV_ty]
+          |> cat_lines
+          |> tracing
+ 
+  fun after_qed thms lthy =
+  let
+    val thm = the_single (flat thms)
+  in
+    typedef_main (Binding.name qty_name, mx, rel_trm, rty, thm) lthy |> snd   
+  end
+in
+  Proof.theorem_i NONE after_qed [[(EQUIV_goal, [])]] lthy
+end
+
 val quottype_parser = 
-    (P.type_args -- P.binding) -- 
-      P.opt_infix -- 
-       (P.$$$ "=" |-- P.term) -- 
+    P.typ -- P.opt_infix -- 
+       (P.$$$ "=" |-- P.typ) -- 
          (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)));
+fun mk_typedef_cmd (((qstr, mx), rstr), rel_str) lthy = 
+let
+  val qty = Syntax.parse_typ lthy qstr
+  val rty = Syntax.parse_typ lthy rstr
+  val rel_trm = Syntax.parse_term lthy rel_str
+                |> Syntax.check_term lthy
+in
+  mk_typedef (qty, mx, rty, rel_trm) lthy  
+end
 
-end;
-*)
+val _ = OuterKeyword.keyword "/"
 
-end;
+val _ = 
+    OuterSyntax.local_theory_to_proof "quotient" 
+      "quotient type definition (requires equivalence proof)"
+         OuterKeyword.thy_goal (quottype_parser >> mk_typedef_cmd)	     
 
-end;
+end; (* local *)
+
+end; (* structure *)
 
 open Quotient
\ No newline at end of file