diff -r a9ee1f240b81 -r 068b430e678f src/HOL/Metis.thy
--- a/src/HOL/Metis.thy	Fri Mar 18 20:35:01 2016 +0100
+++ b/src/HOL/Metis.thy	Fri Mar 18 21:21:09 2016 +0100
@@ -12,7 +12,7 @@
 
 declare [[ML_print_depth = 0]]
 ML_file "~~/src/Tools/Metis/metis.ML"
-declare [[ML_print_depth = 10]]
+declare [[ML_print_depth = 20]]
 
 
 subsection \<open>Literal selection and lambda-lifting helpers\<close>