src/Tools/intuitionistic.ML

--- a/src/Tools/intuitionistic.ML	Thu Jul 25 16:46:53 2013 +0200
+++ b/src/Tools/intuitionistic.ML	Sat Jul 27 16:35:51 2013 +0200
@@ -20,7 +20,7 @@
 val remdups_tac = SUBGOAL (fn (g, i) =>
   let val prems = Logic.strip_assums_hyp g in
     REPEAT_DETERM_N (length prems - length (distinct op aconv prems))
-    (Tactic.ematch_tac [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i)
+    (ematch_tac [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i)
   end);
 
 fun REMDUPS tac = tac THEN_ALL_NEW remdups_tac;