# HG changeset patch
# User wenzelm
# Date 936716207 -7200
# Node ID 257dd777767649cc488c1591caffc0a3022bb595
# Parent  76ed51454609818a92ea6cbd2b08c3991367ee2c
tuned;

diff -r 76ed51454609 -r 257dd7777676 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Tue Sep 07 16:56:10 1999 +0200
+++ b/src/Pure/Isar/local_defs.ML	Tue Sep 07 16:56:47 1999 +0200
@@ -17,7 +17,7 @@
 struct
 
 
-val refl_tac = Tactic.rtac (standard (Drule.reflexive_thm RS Drule.triv_goal));
+val refl_tac = Tactic.rtac (Drule.standard (Drule.reflexive_thm RS Drule.triv_goal));
 
 
 fun gen_def fix prep_term match_binds raw_name atts ((x, raw_T), (raw_rhs, raw_pats)) state =