# HG changeset patch
# User haftmann
# Date 1236757547 -3600
# Node ID 836b71e950b52c7be9b62c0ae47872d00c53633e
# Parent  42ea5d85edccd17e1ad79788e167b39309da1403
avoid inspecting pretty output

diff -r 42ea5d85edcc -r 836b71e950b5 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Wed Mar 11 08:45:47 2009 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Wed Mar 11 08:45:47 2009 +0100
@@ -677,15 +677,14 @@
       val thy = ProofContext.theory_of ctxt;
       val (vs, cos) = the_datatype_spec thy dtco;
       val ty = Type (dtco, map TFree vs);
-      fun pretty_typ_br ty =
-        let
-          val p = Syntax.pretty_typ ctxt ty;
-          val s = explode (Pretty.str_of p);  (* FIXME do not inspect pretty output! *)
-        in if member (op =) s " " then Pretty.enclose "(" ")" [p] else p end;
+      fun pretty_typ_bracket (ty as Type (_, _ :: _)) =
+            Pretty.enclose "(" ")" [Syntax.pretty_typ ctxt ty]
+        | pretty_typ_bracket ty =
+            Syntax.pretty_typ ctxt ty;
       fun pretty_constr (co, tys) =
         (Pretty.block o Pretty.breaks)
           (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
-            map pretty_typ_br tys);
+            map pretty_typ_bracket tys);
       val pretty_datatype =
         Pretty.block
           (Pretty.command "datatype" :: Pretty.brk 1 ::