--- 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