--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Thu May 30 08:27:51 2013 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Thu May 30 12:35:40 2013 +0200
@@ -213,8 +213,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 (Raw_Simplifier.rewrite_rule
- [if_beta RS @{thm eq_reflection}]) intros
+ val intros = map (rewrite_rule [if_beta RS @{thm eq_reflection}]) intros
val _ = print_specs options thy "normalized intros" intros
(*val intros = maps (split_cases thy) intros*)
val (intros', (local_defs, thy')) = flatten_intros constname intros thy