diff -r 5dffcd087e30 -r 14682786c356 quotient_def.ML
--- a/quotient_def.ML	Sun Dec 06 00:00:47 2009 +0100
+++ b/quotient_def.ML	Sun Dec 06 06:39:32 2009 +0100
@@ -81,17 +81,7 @@
 
 fun make_def qconst_bname qty mx attr rhs lthy =
 let
-  val rty = fastype_of rhs
-  val (arg_rtys, res_rty) = strip_type rty
-  val (arg_qtys, res_qty) = strip_type qty
-  
-  val rep_fns = map (get_fun repF lthy) (arg_rtys ~~ arg_qtys)
-  val abs_fn  = get_fun absF lthy (res_rty, res_qty)
-
-  fun mk_fun_map t s =  
-        Const (@{const_name "fun_map"}, dummyT) $ t $ s
-
-  val absrep_trm = (fold_rev mk_fun_map rep_fns abs_fn $ rhs)
+  val absrep_trm = get_fun absF lthy (fastype_of rhs, qty) $ rhs
                    |> Syntax.check_term lthy 
 
   val ((trm, thm), lthy') = define qconst_bname mx attr absrep_trm lthy