--- a/src/HOL/Tools/Function/termination.ML Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Tools/Function/termination.ML Fri May 13 22:55:00 2011 +0200
@@ -297,7 +297,7 @@
THEN' ((rtac @{thm refl}) (* unification instantiates all Vars *)
ORELSE' ((rtac @{thm conjI})
THEN' (rtac @{thm refl})
- THEN' (blast_tac (claset_of ctxt)))) (* Solve rest of context... not very elegant *)
+ THEN' (blast_tac ctxt))) (* Solve rest of context... not very elegant *)
) i
in
((PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])