# HG changeset patch
# User blanchet
# Date 1504821786 -7200
# Node ID dbe1dc1f00161da25e66a47bf4ae4d554346ef01
# Parent  56456f3888674fc3117b0f862f09fa3951c07cd1
tuned whitespace in Nunchaku output

diff -r 56456f388867 -r dbe1dc1f0016 src/HOL/Tools/Nunchaku/nunchaku_collect.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_collect.ML	Fri Sep 08 00:03:00 2017 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_collect.ML	Fri Sep 08 00:03:06 2017 +0200
@@ -1073,7 +1073,7 @@
 
 fun str_of_isa_rec_spec ctxt {const, props, pat_complete} =
   str_of_isa_term_with_type ctxt const ^ (if pat_complete then " [pat_complete]" else "") ^
-  " :=\n " ^ space_implode ";\n " (map (Syntax.string_of_term ctxt) props);
+  " :=\n  " ^ space_implode ";\n  " (map (Syntax.string_of_term ctxt) props);
 
 fun str_of_isa_consts_spec ctxt {consts, props} =
   space_implode " and\n     " (map (str_of_isa_term_with_type ctxt) consts) ^ " :=\n  " ^