# HG changeset patch
# User ballarin
# Date 1090935599 -7200
# Node ID 8beb68a7afd9fa9091875f6da929799d356c8f4f
# Parent  89840837108e20b5552986677d1d29dd8a5caa75
*** empty log message ***

diff -r 89840837108e -r 8beb68a7afd9 src/Provers/trancl.ML
--- a/src/Provers/trancl.ML	Mon Jul 26 17:34:52 2004 +0200
+++ b/src/Provers/trancl.ML	Tue Jul 27 15:39:59 2004 +0200
@@ -119,7 +119,7 @@
 |   makeStep (RTrans (a,_,p), Trans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.rtrancl_trancl_trancl))
 |   makeStep (Trans (a,_,p), RTrans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.trancl_rtrancl_trancl))   
 |   makeStep (RTrans (a,_,p), RTrans(_,c,q))  = RTrans (a,c, Thm ([p,q], Cls.rtrancl_trans))  
-|   makeStep (a,b) = error ("makeStep: internal error: undefined case\n"^(makestring a) ^"\n" ^ (makestring b));
+|   makeStep (a,b) = error ("trancl_tac: internal error in makeStep: undefined case");
 
 (* ******************************************************************* *)
 (*                                                                     *)