# 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 " ^