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