--- a/QuotMain.thy	Wed Sep 23 16:44:56 2009 +0200
+++ b/QuotMain.thy	Wed Sep 23 16:57:56 2009 +0200
@@ -881,12 +881,9 @@
           end
       | build_aux x =
           if is_const x then maybe_mk_rep_abs x else x
-    val prems = (*map HOLogic.dest_Trueprop*) (Thm.prems_of thm);
-    val concl = (*HOLogic.dest_Trueprop*) (Thm.concl_of thm);
-    val concl2 = Logic.list_implies (prems, concl)
-(*    val concl2 = fold (fn a => fn c => HOLogic.mk_imp (a, c)) prems concl*)
+    val concl2 = term_of (#prop (crep_thm thm))
   in
-  Logic.mk_equals ( (build_aux concl2), concl2)
+  Logic.mk_equals ((build_aux concl2), concl2)
 end *}
 
 ML {* val emptyt = (symmetric (unlam_def  @{context} @{thm EMPTY_def})) *}