| changeset 62672 | 068b430e678f |
| parent 60758 | d8d85a8172b5 |
| child 62711 | 09df6a51ad3c |
--- 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>