diff -r 61668e617a3b -r ba14eafef077 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Sun May 15 18:00:08 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Sun May 15 18:59:27 2011 +0200
@@ -98,7 +98,7 @@
           val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp}
           val atom' = Raw_Simplifier.rewrite_term thy
             (map (fn th => th RS @{thm eq_reflection}) [@{thm if_bool_eq_disj}, if_beta]) [] atom
-          val _ = assert (not (atom = atom'))
+          val _ = @{assert} (not (atom = atom'))
         in
           flatten constname atom' (defs, thy)
         end