diff -r e84d900cd287 -r 59203adfc33f src/FOL/ex/Miniscope.thy
--- a/src/FOL/ex/Miniscope.thy	Thu Oct 30 16:20:46 2014 +0100
+++ b/src/FOL/ex/Miniscope.thy	Thu Oct 30 16:55:29 2014 +0100
@@ -65,7 +65,7 @@
 
 ML {*
 val mini_ss = simpset_of (@{context} addsimps @{thms mini_simps});
-fun mini_tac ctxt = rtac @{thm ccontr} THEN' asm_full_simp_tac (put_simpset mini_ss ctxt);
+fun mini_tac ctxt = resolve_tac @{thms ccontr} THEN' asm_full_simp_tac (put_simpset mini_ss ctxt);
 *}
 
 end