--- a/src/HOL/MicroJava/J/JTypeSafe.thy Fri Dec 13 23:53:02 2013 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Sat Dec 14 17:28:05 2013 +0100
@@ -325,7 +325,7 @@
apply( fast intro: hext_trans)
-apply( tactic prune_params_tac)
+apply( tactic "prune_params_tac @{context}")
-- "Level 52"
-- "1 Call"