diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/Tools/TFL/casesplit.ML
--- a/src/HOL/Tools/TFL/casesplit.ML	Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/Tools/TFL/casesplit.ML	Mon Sep 06 19:13:10 2010 +0200
@@ -32,9 +32,9 @@
 val dest_Trueprop = HOLogic.dest_Trueprop;
 val mk_Trueprop = HOLogic.mk_Trueprop;
 
-val atomize = thms "induct_atomize";
-val rulify = thms "induct_rulify";
-val rulify_fallback = thms "induct_rulify_fallback";
+val atomize = @{thms induct_atomize};
+val rulify = @{thms induct_rulify};
+val rulify_fallback = @{thms induct_rulify_fallback};
 
 end;