# HG changeset patch
# User clasohm
# Date 796561679 -7200
# Node ID 33e3054b2871154b1387a10a4a2e3e54be30bbc7
# Parent  a29142d703bcb4e8e7619f76a13d7f381527e337
removed unnecessary parentheses from the generated rules

diff -r a29142d703bc -r 33e3054b2871 src/HOL/datatype.ML
--- a/src/HOL/datatype.ML	Thu Mar 30 08:54:17 1995 +0200
+++ b/src/HOL/datatype.ML	Thu Mar 30 13:07:59 1995 +0200
@@ -209,7 +209,7 @@
 	let val arity = length vns;
 	  val body  = "z" ^ string_of_int(c_nr);
 	  val args1 = if arity=0 then ""
-		      else parens (Args ("y", ") (", y_nr, y_nr+arity-1));
+		      else " " ^ Args ("y", " ", y_nr, y_nr+arity-1);
 	  val args2 = if arity=0 then ""
 		      else "(% " ^ Args ("y", " ", y_nr, y_nr+arity-1) 
 			^ ". ";
@@ -224,8 +224,8 @@
       
       val xrules =
 	let val (first_part, scnd_part) = calc_xrules 1 1 cons_list
-	in  [("logic", "case x of " ^ first_part) <->
-	     ("logic", tname ^ "_case " ^ scnd_part ^ " x" )]
+	in [("logic", "case x of " ^ first_part) <->
+	     ("logic", tname ^ "_case " ^ scnd_part ^ " x")]
 	end;
 
      (*type declarations for constructors*)
@@ -269,10 +269,10 @@
       val t_case = tname ^ "_case";
 
       fun case_rule n (id, name, _, vns, _) =
-	let val args =  opt_parens(space_implode ") (" vns)
+	let val args = if vns = [] then "" else " " ^ space_implode " " vns
 	in (t_case ^ "_" ^ id,
-	    t_case ^ " (" ^ Args("f", ") (", 1, num_of_cons)
-	    ^ ") (" ^ name ^ args ^ ") = f"^string_of_int(n) ^ args)
+	    t_case ^ " " ^ Args("f", " ", 1, num_of_cons)
+	    ^ " (" ^ name ^ args ^ ") = f"^string_of_int(n) ^ args)
 	end
 
       fun case_rules n (c :: cs) = case_rule n c :: case_rules(n+1) cs