diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/Import/shuffler.ML	Mon Sep 06 19:13:10 2010 +0200
@@ -346,7 +346,7 @@
 fun beta_fun thy assume t =
     SOME (Thm.beta_conversion true (cterm_of thy t))
 
-val meta_sym_rew = thm "refl"
+val meta_sym_rew = @{thm refl}
 
 fun equals_fun thy assume t =
     case t of