diff -r 0c5cd369a643 -r 50b60f501b05 src/FOL/ex/Miniscope.thy
--- a/src/FOL/ex/Miniscope.thy	Tue Feb 10 14:29:36 2015 +0100
+++ b/src/FOL/ex/Miniscope.thy	Tue Feb 10 14:48:26 2015 +0100
@@ -65,7 +65,8 @@
 
 ML {*
 val mini_ss = simpset_of (@{context} addsimps @{thms mini_simps});
-fun mini_tac ctxt = resolve_tac @{thms ccontr} THEN' asm_full_simp_tac (put_simpset mini_ss ctxt);
+fun mini_tac ctxt =
+  resolve_tac ctxt @{thms ccontr} THEN' asm_full_simp_tac (put_simpset mini_ss ctxt);
 *}
 
 end