--- a/FSet.thy	Thu Nov 05 10:46:54 2009 +0100
+++ b/FSet.thy	Thu Nov 05 13:47:04 2009 +0100
@@ -172,6 +172,8 @@
 term fmap
 thm fmap_def
 
+ML {* prop_of @{thm fmap_def} *}
+
 ML {* val defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def FOLD_def} *}
 ML {* val consts = lookup_quot_consts defs *}
 ML {* val defs_sym = add_lower_defs @{context} defs *}

--- a/IntEx.thy	Thu Nov 05 10:46:54 2009 +0100
+++ b/IntEx.thy	Thu Nov 05 13:47:04 2009 +0100
@@ -23,6 +23,8 @@
 term ZERO
 thm ZERO_def
 
+ML {* prop_of @{thm ZERO_def} *}
+
 quotient_def 
   ONE::"my_int"
 where
@@ -44,6 +46,10 @@
 term PLUS
 thm PLUS_def
 
+ML {* toplevel_pp ["typ"] "ProofDisplay.pp_typ Pure.thy"; *}
+
+ML {* prop_of @{thm PLUS_def} *}
+
 fun
   my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
 where

--- a/QuotTest.thy	Thu Nov 05 10:46:54 2009 +0100
+++ b/QuotTest.thy	Thu Nov 05 13:47:04 2009 +0100
@@ -77,27 +77,19 @@
 print_quotients
 
 ML {*
-Toplevel.context_of;
-Toplevel.keep
-*}
-
-ML {*
   get_fun repF [(@{typ qt}, @{typ qt})] @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"}
-  |> fst
   |> Syntax.string_of_term @{context}
   |> writeln
 *}
 
 ML {*
   get_fun absF [(@{typ qt}, @{typ t})] @{context} @{typ "qt * nat"}
-  |> fst
   |> Syntax.string_of_term @{context}
   |> writeln
 *}
 
 ML {*
   get_fun absF [(@{typ qt}, @{typ t})] @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"}
-  |> fst
   |> Syntax.pretty_term @{context}
   |> Pretty.string_of
   |> writeln

--- a/quotient.ML	Thu Nov 05 10:46:54 2009 +0100
+++ b/quotient.ML	Thu Nov 05 13:47:04 2009 +0100
@@ -1,7 +1,7 @@
 signature QUOTIENT =
 sig
-  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 quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state
+  val quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state
   val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory
   val note: binding * thm -> local_theory -> thm * local_theory
 end;
@@ -190,7 +190,7 @@
 (* - the type to be quotient                                *)
 (* - the relation according to which the type is quotient   *)
 
-fun mk_quotient_type quot_list lthy = 
+fun quotient_type quot_list lthy = 
 let
   fun mk_goal (rty, rel) =
   let
@@ -207,7 +207,7 @@
   theorem after_qed goals lthy
 end
            
-fun mk_quotient_type_cmd spec lthy = 
+fun quotient_type_cmd spec lthy = 
 let
   fun parse_spec (((qty_str, mx), rty_str), rel_str) =
   let
@@ -218,7 +218,7 @@
     ((qty_name, mx), (rty, rel))
   end
 in
-  mk_quotient_type (map parse_spec spec) lthy
+  quotient_type (map parse_spec spec) lthy
 end
 
 val quotspec_parser = 
@@ -232,7 +232,7 @@
 val _ = 
     OuterSyntax.local_theory_to_proof "quotient" 
       "quotient type definitions (requires equivalence proofs)"
-         OuterKeyword.thy_goal (quotspec_parser >> mk_quotient_type_cmd)
+         OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd)
 
 end; (* structure *)
 

--- a/quotient_def.ML	Thu Nov 05 10:46:54 2009 +0100
+++ b/quotient_def.ML	Thu Nov 05 13:47:04 2009 +0100
@@ -2,7 +2,7 @@
 signature QUOTIENT_DEF =
 sig
   datatype flag = absF | repF
-  val get_fun: flag -> (typ * typ) list -> Proof.context -> typ -> term * (typ * typ)
+  val get_fun: flag -> (typ * typ) list -> Proof.context -> typ -> term
   val make_def: binding -> term -> typ -> mixfix -> Attrib.binding -> (typ * typ) list ->
     Proof.context -> (term * thm) * local_theory
 
@@ -38,68 +38,54 @@
 fun get_fun flag qenv lthy ty =
 let
   
-  fun get_fun_aux s fs_tys =
-  let
-    val (fs, tys) = split_list fs_tys
-    val (otys, ntys) = split_list tys
-    val oty = Type (s, otys)
-    val nty = Type (s, ntys)
-    val ftys = map (op -->) tys
-  in
+  fun get_fun_aux s fs =
    (case (maps_lookup (ProofContext.theory_of lthy) s) of
-      SOME info => (list_comb (Const (#mapfun info, ftys ---> (oty --> nty)), fs), (oty, nty))
+      SOME info => list_comb (Const (#mapfun info, dummyT), fs)
     | NONE      => error ("no map association for type " ^ s))
-  end
 
-  fun get_fun_fun fs_tys =
-  let
-    val (fs, tys) = split_list fs_tys
-    val ([oty1, oty2], [nty1, nty2]) = split_list tys
-    val oty = nty1 --> oty2
-    val nty = oty1 --> nty2
-    val ftys = map (op -->) tys
-  in
-    (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty))
-  end
-
-  fun get_const flag (qty, rty) =
+  fun get_const flag qty =
   let 
     val thy = ProofContext.theory_of lthy
     val qty_name = Long_Name.base_name (fst (dest_Type qty))
   in
     case flag of
-      absF => (Const (Sign.full_bname thy ("ABS_" ^ qty_name), rty --> qty), (rty, qty))
-    | repF => (Const (Sign.full_bname thy ("REP_" ^ qty_name), qty --> rty), (qty, rty))
+      absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT)
+    | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT)
   end
 
   fun mk_identity ty = Abs ("", ty, Bound 0)
 
 in
   if (AList.defined (op=) qenv ty)
-  then (get_const flag (the (Quotient_Info.lookup_qenv (op=) qenv ty)))
+  then (get_const flag ty)
   else (case ty of
-          TFree _ => (mk_identity ty, (ty, ty))
-        | Type (_, []) => (mk_identity ty, (ty, ty)) 
+          TFree _ => mk_identity ty
+        | Type (_, []) => mk_identity ty 
         | Type ("fun" , [ty1, ty2]) => 
-                 get_fun_fun [get_fun (negF flag) qenv lthy ty1, get_fun flag qenv lthy ty2]
+            let
+              val fs_ty1 = get_fun (negF flag) qenv lthy ty1
+              val fs_ty2 = get_fun flag qenv lthy ty2
+            in  
+              get_fun_aux "fun" [fs_ty1, fs_ty2]
+            end 
         | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys)
-        | _ => raise ERROR ("no type variables"))
+        | _ => error ("no type variables allowed"))
 end
 
 fun make_def nconst_bname rhs qty mx attr qenv lthy =
 let
   val (arg_tys, res_ty) = strip_type qty
 
-  val rep_fns = map (fst o get_fun repF qenv lthy) arg_tys
-  val abs_fn  = (fst o get_fun absF qenv lthy) res_ty
+  val rep_fns = map (get_fun repF qenv lthy) arg_tys
+  val abs_fn  = (get_fun absF qenv lthy) res_ty
 
-  fun mk_fun_map t s = 
+  fun mk_fun_map t s =  
         Const (@{const_name "fun_map"}, dummyT) $ t $ s
 
-  val absrep_fn = fold_rev mk_fun_map rep_fns abs_fn
-                  |> Syntax.check_term lthy 
+  val absrep_trm = (fold_rev mk_fun_map rep_fns abs_fn $ rhs)
+                   |> Syntax.check_term lthy 
 in
-  define nconst_bname mx attr (absrep_fn $ rhs) lthy
+  define nconst_bname mx attr absrep_trm lthy
 end
 
 
@@ -131,21 +117,21 @@
   val global_qenv = Quotient_Info.mk_qenv lthy
   val thy = ProofContext.theory_of lthy
 
-  fun is_inst thy (qty, rty) (qty', rty') =
-  if Sign.typ_instance thy (qty, qty')
-  then let
-         val inst = Sign.typ_match thy (qty', qty) Vartab.empty
-       in
-         rty = Envir.subst_type inst rty'       
-       end
-  else false
+  fun is_inst (qty, rty) (qty', rty') =
+    if Sign.typ_instance thy (qty, qty')
+    then let
+           val inst = Sign.typ_match thy (qty', qty) Vartab.empty
+         in
+           rty = Envir.subst_type inst rty'       
+         end
+    else false
 
   fun chk_inst (qty, rty) = 
-    if exists (is_inst thy (qty, rty)) global_qenv 
+    if exists (is_inst (qty, rty)) global_qenv 
     then true
     else error_msg lthy (qty, rty)
 in
-  forall chk_inst qenv
+  map chk_inst qenv
 end