--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Thu May 30 08:27:51 2013 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Thu May 30 12:35:40 2013 +0200
@@ -127,7 +127,7 @@
fun param_rewrite prem =
param = snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of prem)))
val SOME rew_eq = find_first param_rewrite prems'
- val param_prem' = Raw_Simplifier.rewrite_rule
+ val param_prem' = rewrite_rule
(map (fn th => th RS @{thm eq_reflection})
[rew_eq RS @{thm sym}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}])
param_prem