src/Pure/Isar/local_defs.ML
changeset 7502 257dd7777676
parent 7416 a98963d70f81
child 7667 22dc8b2455b8
--- 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 =