# HG changeset patch
# User blanchet
# Date 1504821741 -7200
# Node ID 0916eb2dbaca7fa9530663652e1e678d8b18fb55
# Parent  1eb8e87f7f8bb9306a9814bcc69fc8761a7998c3
properly parenthesize copy types in Nunchaku

diff -r 1eb8e87f7f8b -r 0916eb2dbaca src/HOL/Tools/Nunchaku/nunchaku_problem.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_problem.ML	Fri Sep 08 00:02:20 2017 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_problem.ML	Fri Sep 08 00:02:21 2017 +0200
@@ -714,7 +714,9 @@
   str_of_ty abs_ty ^ " " ^ nun_assign ^ " " ^ str_of_ty rep_ty ^
   (case subset of
     NONE => ""
-  | SOME s => if is_triv_subset s then "" else "\n  " ^ nun_subset ^ " " ^ str_of_tm s) ^
+  | SOME s =>
+    if is_triv_subset s then ""
+    else "\n  " ^ nun_subset ^ " " ^ nun_parens_if_space (str_of_tm s)) ^
   (* TODO: use nun_quotient when possible *)
   (case quotient of
     NONE => ""