--- a/LamEx.thy	Tue Oct 27 14:59:00 2009 +0100
+++ b/LamEx.thy	Tue Oct 27 15:00:15 2009 +0100
@@ -17,8 +17,11 @@
 | a3: "\<lbrakk>t \<approx> ([(a,b)]\<bullet>s); a\<sharp>s\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s"
 
 quotient lam = rlam / alpha
+apply -
 sorry
 
+print_quotients
+
 local_setup {*
   make_const_def @{binding Var} @{term "rVar"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #>
   make_const_def @{binding App} @{term "rApp"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #>

--- a/QuotMain.thy	Tue Oct 27 14:59:00 2009 +0100
+++ b/QuotMain.thy	Tue Oct 27 15:00:15 2009 +0100
@@ -137,6 +137,8 @@
 
 section {* type definition for the quotient type *}
 
+ML {* Proof.theorem_i NONE *}
+
 use "quotient.ML"
 
 declare [[map list = (map, LIST_REL)]]
@@ -150,7 +152,7 @@
 ML {*
 val quot_def_parser = 
   (OuterParse.$$$ "(" |-- OuterParse.$$$ "with" |-- 
-    ((OuterParse.list1 OuterParse.binding) --| OuterParse.$$$ ")")) --
+    ((OuterParse.list1 OuterParse.typ) --| OuterParse.$$$ ")")) --
       (OuterParse.binding -- 
         Scan.option (OuterParse.$$$ "::" |-- OuterParse.typ) -- 
          OuterParse.mixfix --| OuterParse.where_ -- SpecParse.spec)

--- a/quotient.ML	Tue Oct 27 14:59:00 2009 +0100
+++ b/quotient.ML	Tue Oct 27 15:00:15 2009 +0100
@@ -1,7 +1,7 @@
 signature QUOTIENT =
 sig
   type maps_info = {mapfun: string, relfun: string}
-  type quotient_info = {qtyp: typ, rtyp: typ, rel: term}
+  type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
   val mk_quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state
   val mk_quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state
   val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory
@@ -11,8 +11,8 @@
   val maps_update: string -> maps_info -> Proof.context -> Proof.context                           
   val print_quotdata: Proof.context -> unit
   val quotdata_lookup: theory -> quotient_info list
-  val quotdata_update_thy: (typ * typ * term) -> theory -> theory
-  val quotdata_update: (typ * typ * term) -> Proof.context -> Proof.context
+  val quotdata_update_thy: (typ * typ * term * thm) -> theory -> theory
+  val quotdata_update: (typ * typ * term * thm) -> Proof.context -> Proof.context
 end;
 
 structure Quotient: QUOTIENT =
@@ -61,7 +61,7 @@
 
 
 (* info about the quotient types *)
-type quotient_info = {qtyp: typ, rtyp: typ, rel: term}
+type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
 
 structure QuotData = TheoryDataFun
   (type T = quotient_info list
@@ -72,22 +72,24 @@
 
 val quotdata_lookup = QuotData.get
 
-fun quotdata_update_thy (qty, rty, rel) thy = 
-      QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel}::ls) thy
+fun quotdata_update_thy (qty, rty, rel, equiv_thm) thy = 
+      QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm}::ls) thy
 
-fun quotdata_update (qty, rty, rel) ctxt = 
-      ProofContext.theory (quotdata_update_thy (qty, rty, rel)) ctxt
+fun quotdata_update (qty, rty, rel, equiv_thm) ctxt = 
+      ProofContext.theory (quotdata_update_thy (qty, rty, rel, equiv_thm)) ctxt
 
 fun print_quotdata ctxt =
 let
-  fun prt_quot {qtyp, rtyp, rel} = 
+  fun prt_quot {qtyp, rtyp, rel, equiv_thm} = 
       Pretty.block (Library.separate (Pretty.brk 2)
           [Pretty.str ("quotient type:"), 
            Syntax.pretty_typ ctxt qtyp,
            Pretty.str ("raw type:"), 
            Syntax.pretty_typ ctxt rtyp,
            Pretty.str ("relation:"), 
-           Syntax.pretty_term ctxt rel])
+           Syntax.pretty_term ctxt rel,
+           Pretty.str ("equiv. thm:"), 
+           Syntax.pretty_term ctxt (prop_of equiv_thm)])
 in
   QuotData.get (ProofContext.theory_of ctxt)
   |> map prt_quot
@@ -101,7 +103,7 @@
 
 
 
-(* wrappers for define and note *)
+(* wrappers for define, note and theorem_i *)
 fun define (name, mx, rhs) lthy =
 let
   val ((rhs, (_ , thm)), lthy') =
@@ -117,6 +119,13 @@
   (thm', lthy')
 end
 
+fun theorem after_qed goals ctxt =
+let
+  val goals' = map (rpair []) goals
+  fun after_qed' thms = after_qed (the_single thms)
+in 
+  Proof.theorem_i NONE after_qed' [goals'] ctxt
+end
 
 
 (* definition of the quotient type *)
@@ -154,7 +163,7 @@
 (* tactic to prove the QUOT_TYPE theorem for the new type *)
 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) =
 let
-  val unfold_mem = MetaSimplifier.rewrite_rule @{thms mem_def}
+  val unfold_mem = MetaSimplifier.rewrite_rule [@{thm mem_def}]
   val rep_thm = #Rep typedef_info |> unfold_mem
   val rep_inv = #Rep_inverse typedef_info
   val abs_inv = #Abs_inverse typedef_info |> unfold_mem
@@ -231,7 +240,7 @@
   val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name
 
   (* storing the quot-info *)
-  val lthy3 = quotdata_update (abs_ty, rty, rel) lthy2
+  val lthy3 = quotdata_update (abs_ty, rty, rel, equiv_thm) lthy2
 
   (* interpretation *)
   val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))
@@ -281,15 +290,29 @@
   let
     val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
   in 
-    (HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel), [])
+    HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel)
   end
 
   val goals = map (mk_goal o snd) quot_list
               
   fun after_qed thms lthy =
-    fold_map mk_typedef_main (quot_list ~~ (flat thms)) lthy |> snd
+    fold_map mk_typedef_main (quot_list ~~ thms) lthy |> snd
 in
-  Proof.theorem_i NONE after_qed [goals] lthy
+  theorem after_qed goals lthy
+end
+           
+fun mk_quotient_type_cmd spec lthy = 
+let
+  fun parse_spec (((qty_str, mx), rty_str), rel_str) =
+  let
+    val qty_name = Binding.name qty_str
+    val rty = Syntax.parse_typ lthy rty_str |> Syntax.check_typ lthy
+    val rel = Syntax.parse_term lthy rel_str |> Syntax.check_term lthy
+  in
+    ((qty_name, mx), (rty, rel))
+  end
+in
+  mk_quotient_type (map parse_spec spec) lthy
 end
 
 val quotspec_parser = 
@@ -297,21 +320,6 @@
      (OuterParse.short_ident -- OuterParse.opt_infix -- 
        (OuterParse.$$$ "=" |-- OuterParse.typ) -- 
          (OuterParse.$$$ "/" |-- OuterParse.term))
-           
-fun mk_quotient_type_cmd spec lthy = 
-let
-  fun parse_spec (((qty_str, mx), rty_str), rel_str) =
-  let
-    val qty_name = Binding.name qty_str
-    val rty = Syntax.parse_typ lthy rty_str
-    val rel = Syntax.parse_term lthy rel_str
-              |> Syntax.check_term lthy
-  in
-    ((qty_name, mx), (rty, rel))
-  end
-in
-  mk_quotient_type (map parse_spec spec) lthy
-end
 
 val _ = OuterKeyword.keyword "/"