src/HOL/Tools/Function/termination.ML

--- a/src/HOL/Tools/Function/termination.ML	Fri Dec 13 23:53:02 2013 +0100
+++ b/src/HOL/Tools/Function/termination.ML	Sat Dec 14 17:28:05 2013 +0100
@@ -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 rewrite_goal_tac Un_aci_simps 1) st  (* eliminate duplicates *)
+     THEN rewrite_goal_tac ctxt Un_aci_simps 1) st  (* eliminate duplicates *)
   end
 
 end