diff -r d808005e6e08 -r 92706a69dacc src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Wed Oct 10 18:39:38 2001 +0200
+++ b/src/Pure/Isar/local_defs.ML	Wed Oct 10 18:40:46 2001 +0200
@@ -22,7 +22,7 @@
 
 local
 
-val refl_tac = Tactic.rtac (Drule.standard (Drule.reflexive_thm RS Drule.triv_goal));
+val refl_tac = Tactic.rtac (Drule.reflexive_thm RS Drule.triv_goal);
 
 fun dest_lhs cprop =
   let val x = #1 (Logic.dest_equals (Logic.dest_goal (Thm.term_of cprop)))