diff -r 11e7ee2ca77f -r e1fce873b814 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Fri Dec 17 16:25:21 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Fri Dec 17 17:08:56 2010 +0100
@@ -96,7 +96,7 @@
       (Const (@{const_name If}, _)) =>
         let
           val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp}
-          val atom' = MetaSimplifier.rewrite_term thy
+          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'))
         in
@@ -212,7 +212,7 @@
           error ("unexpected specification for constant " ^ quote constname ^ ":\n"
             ^ commas (map (quote o Display.string_of_thm_global thy) specs))
       val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp}
-      val intros = map (MetaSimplifier.rewrite_rule
+      val intros = map (Raw_Simplifier.rewrite_rule
           [if_beta RS @{thm eq_reflection}]) intros
       val _ = print_specs options thy "normalized intros" intros
       (*val intros = maps (split_cases thy) intros*)