src/HOL/SMT.thy

--- a/src/HOL/SMT.thy	Fri Apr 24 23:05:33 2015 +0200
+++ b/src/HOL/SMT.thy	Sat Apr 25 09:48:06 2015 +0200
@@ -49,7 +49,7 @@
 *}
 
 method_setup moura = {*
- Scan.succeed (SIMPLE_METHOD' o moura_tac)
+  Scan.succeed (SIMPLE_METHOD' o moura_tac)
 *} "solve skolemization goals, especially those arising from Z3 proofs"
 
 hide_fact (open) choices bchoices