# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1254734672 -7200
# Node ID 58384c90a5e53882c17a6d56df1ff2e1c2e37ccd
# Parent  1585a60b076d56b5f7171f7a56917fc16c5eb596
used prop_of to get the term of a theorem (replaces crep_thm)

diff -r 1585a60b076d -r 58384c90a5e5 QuotMain.thy
--- a/QuotMain.thy	Fri Oct 02 11:10:21 2009 +0200
+++ b/QuotMain.thy	Mon Oct 05 11:24:32 2009 +0200
@@ -1194,7 +1194,7 @@
 
 thm leqi4_lift
 ML {*
-  val (nam, typ) = (hd (Term.add_vars (term_of (#prop (crep_thm @{thm leqi4_lift}))) []))
+  val (nam, typ) = hd (Term.add_vars (prop_of @{thm leqi4_lift}) [])
   val (_, l) = dest_Type typ
   val t = Type ("QuotMain.fset", l)
   val v = Var (nam, t)
@@ -1212,7 +1212,7 @@
 (*
 thm card_suc
 ML {*
-  val (nam, typ) = (hd (tl (Term.add_vars (term_of (#prop (crep_thm @{thm card_suc}))) [])))
+  val (nam, typ) = hd (tl (Term.add_vars (prop_of @{thm card_suc})) [])
   val (_, l) = dest_Type typ
   val t = Type ("QuotMain.fset", l)
   val v = Var (nam, t)