# HG changeset patch
# User berghofe
# Date 1002732046 -7200
# Node ID 92706a69daccdf59de6afe2864bd0f60ae6ff598
# Parent  d808005e6e085fb7c977c0cc3a7d3ad0bde2f76b
Removed unnecessary application of Drule.standard.

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)))