diff -r 76979adf0b96 -r 384bfd19ee61 src/Doc/IsarImplementation/Tactic.thy
--- a/src/Doc/IsarImplementation/Tactic.thy	Mon Feb 17 21:37:41 2014 +0100
+++ b/src/Doc/IsarImplementation/Tactic.thy	Mon Feb 17 22:39:20 2014 +0100
@@ -920,9 +920,8 @@
   "thm"} has fewer than @{text "n"} premises.
 
   \item @{ML Thm.eq_thm}~@{text "(thm\<^sub>1, thm\<^sub>2)"} reports whether @{text
-  "thm\<^sub>1"} and @{text "thm\<^sub>2"} are equal.  Both theorems must have
-  compatible background theories.  Both theorems must have the same
-  conclusions, the same set of hypotheses, and the same set of sort
+  "thm\<^sub>1"} and @{text "thm\<^sub>2"} are equal.  Both theorems must have the
+  same conclusions, the same set of hypotheses, and the same set of sort
   hypotheses.  Names of bound variables are ignored as usual.
 
   \item @{ML Thm.eq_thm_prop}~@{text "(thm\<^sub>1, thm\<^sub>2)"} reports whether