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)