diff -r 37f7dc85b61b -r 3d7a9d4d2bb6 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Fri Dec 11 15:49:15 2009 +0100
+++ b/Quot/QuotMain.thy	Fri Dec 11 15:58:15 2009 +0100
@@ -1082,7 +1082,7 @@
 val msg1 = "Regularize proof failed."
 val msg2 = cat_lines ["Injection proof failed.", 
                       "This is probably due to missing respects lemmas.",
-                      "Try invoking the injection_tac manually to see", 
+                      "Try invoking the injection method manually to see", 
                       "which lemmas are missing."]
 val msg3 = "Cleaning proof failed."