src/HOL/Tools/Predicate_Compile/core_data.ML

--- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Thu Jul 25 16:46:53 2013 +0200
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Sat Jul 27 16:35:51 2013 +0200
@@ -236,7 +236,7 @@
       (PEEK nprems_of
         (fn n =>
           ALLGOALS (fn i =>
-            Simplifier.rewrite_goal_tac [@{thm split_paired_all}] i
+            rewrite_goal_tac [@{thm split_paired_all}] i
             THEN (SUBPROOF (instantiate i n) ctxt i))))
   in
     Goal.prove ctxt (Term.add_free_names cases_rule []) [] cases_rule (fn _ => tac)