# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1253717876 -7200
# Node ID 322ae3432548db0ffb5f700b3a0b0382222f8dfb
# Parent  e35198635d6410bfe46f716e12d925e31f88533e
Proper code for getting the prop out of the theorem.

diff -r e35198635d64 -r 322ae3432548 QuotMain.thy
--- 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})) *}