diff -r 253f6808dabe -r ef59550a55d3 src/HOL/Tools/Function/termination.ML
--- a/src/HOL/Tools/Function/termination.ML	Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Tools/Function/termination.ML	Thu Jul 23 18:44:09 2009 +0200
@@ -303,7 +303,7 @@
           THEN' ((rtac @{thm refl})                       (* unification instantiates all Vars *)
                  ORELSE' ((rtac @{thm conjI})
                           THEN' (rtac @{thm refl})
-                          THEN' (blast_tac (local_claset_of ctxt))))  (* Solve rest of context... not very elegant *)
+                          THEN' (blast_tac (claset_of ctxt))))  (* Solve rest of context... not very elegant *)
           ) i
     in
       ((PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])