# HG changeset patch
# User wenzelm
# Date 869225803 -7200
# Node ID 31186470665fe9fb8bc27fb44d4423445541576d
# Parent  f4b28e25ba997198f606831b7cf4235417bc4b38
tuned warning;
improved comments;

diff -r f4b28e25ba99 -r 31186470665f src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Jul 18 13:36:03 1997 +0200
+++ b/src/Pure/thm.ML	Fri Jul 18 13:36:43 1997 +0200
@@ -627,7 +627,9 @@
   end;
 
 (*Implication introduction
-  A |- B
+    [A]
+     :
+     B
   -------
   A ==> B
 *)
@@ -860,9 +862,9 @@
   end;
 
 (*The combination rule
-  f==g    t==u
-  ------------
-   f(t)==g(u)
+  f == g  t == u
+  --------------
+   f(t) == g(u)
 *)
 fun combination th1 th2 =
   let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1, 
@@ -896,9 +898,9 @@
 
 
 (* Equality introduction
-  A==>B    B==>A
-  --------------
-       A==B
+  A ==> B  B ==> A
+  ----------------
+       A == B
 *)
 fun equal_intr th1 th2 =
   let val Thm{der=der1,maxidx=max1, shyps=shyps1, hyps=hyps1, 
@@ -923,7 +925,7 @@
 
 
 (*The equal propositions rule
-  A==B    A
+  A == B  A
   ---------
       B
 *)
@@ -1423,7 +1425,7 @@
 exception SIMPLIFIER of string * thm;
 
 fun prtm a sign t = (writeln a; writeln (Sign.string_of_term sign t));
-fun prtm_warning a sign t = warning (a ^ "\n" ^ (Sign.string_of_term sign t));
+fun prtm_warning a sign t = (warning a; warning (Sign.string_of_term sign t));
 
 val trace_simp = ref false;