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