--- 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)])