src/HOL/Tools/Function/termination.ML

--- a/src/HOL/Tools/Function/termination.ML	Thu Jul 25 16:46:53 2013 +0200
+++ b/src/HOL/Tools/Function/termination.ML	Sat Jul 27 16:35:51 2013 +0200
@@ -305,7 +305,7 @@
   in
     (PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])
      THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i)
-     THEN Raw_Simplifier.rewrite_goal_tac Un_aci_simps 1) st  (* eliminate duplicates *)
+     THEN rewrite_goal_tac Un_aci_simps 1) st  (* eliminate duplicates *)
   end
 
 end