src/HOL/Import/shuffler.ML

        end
 
 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
         Const("op ==",_) $ u $ v => if Term_Ord.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE
       | _ => NONE