src/HOL/ex/MT.ML

--- a/src/HOL/ex/MT.ML	Mon Nov 27 13:42:30 2006 +0100
+++ b/src/HOL/ex/MT.ML	Mon Nov 27 13:42:33 2006 +0100
@@ -602,7 +602,7 @@
 (* ############################################################ *)
 
 fun excluded_middle_tac sP =
-  res_inst_tac [("Q", sP)] (excluded_middle RS HOL.disjE);
+  res_inst_tac [("Q", sP)] (excluded_middle RS disjE);
 
 Goal "[| ve hastyenv te; v hasty t |] ==> \
 \        ve + {ev |-> v} hastyenv te + {ev |=> t}";