diff -r e6b96b4cde7e -r 0dec18004e75 src/ZF/Cardinal_AC.thy
--- a/src/ZF/Cardinal_AC.thy	Mon Sep 06 19:11:01 2010 +0200
+++ b/src/ZF/Cardinal_AC.thy	Mon Sep 06 19:13:10 2010 +0200
@@ -193,8 +193,8 @@
 
 ML
 {*
-val cardinal_0_iff_0 = thm "cardinal_0_iff_0";
-val cardinal_lt_iff_lesspoll = thm "cardinal_lt_iff_lesspoll";
+val cardinal_0_iff_0 = @{thm cardinal_0_iff_0};
+val cardinal_lt_iff_lesspoll = @{thm cardinal_lt_iff_lesspoll};
 *}
 
 end