# HG changeset patch
# User wenzelm
# Date 951853903 -3600
# Node ID c9b4f1c4781694606420fdb19088ef9b8295f16e
# Parent  463f63a9a7f2591d571d24d823658edbe6ec3740
tuned msgs;

diff -r 463f63a9a7f2 -r c9b4f1c47816 src/HOL/Tools/induct_method.ML
--- a/src/HOL/Tools/induct_method.ML	Tue Feb 29 10:57:30 2000 +0100
+++ b/src/HOL/Tools/induct_method.ML	Tue Feb 29 20:51:43 2000 +0100
@@ -38,7 +38,7 @@
 
 fun print_rules kind rs =
   let val thms = map snd (NetRules.rules rs)
-  in Pretty.writeln (Pretty.big_list (kind ^ " rules:") (map Display.pretty_thm thms)) end;
+  in Pretty.writeln (Pretty.big_list kind (map Display.pretty_thm thms)) end;
 
 
 (* theory data kind 'HOL/induct_method' *)
@@ -57,10 +57,10 @@
       (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)));
 
   fun print _ ((casesT, casesS), (inductT, inductS)) =
-    (print_rules "type cases" casesT;
-      print_rules "set cases" casesS;
-      print_rules "type induct" inductT;
-      print_rules "set induct" inductS);
+    (print_rules "type cases:" casesT;
+      print_rules "set cases:" casesS;
+      print_rules "type induct:" inductT;
+      print_rules "set induct:" inductS);
 end;
 
 structure GlobalInduct = TheoryDataFun(GlobalInductArgs);