src/Provers/trancl.ML
changeset 15078 8beb68a7afd9
parent 15076 4b3d280ef06a
child 15098 0726e7b15618
--- 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");
 
 (* ******************************************************************* *)
 (*                                                                     *)