src/ZF/ind_syntax.ML

--- a/src/ZF/ind_syntax.ML	Fri Oct 16 10:55:07 2009 +0200
+++ b/src/ZF/ind_syntax.ML	Sat Oct 17 00:52:37 2009 +0200
@@ -115,7 +115,7 @@
   | tryres (th, []) = raise THM("tryres", 0, [th]);
 
 fun gen_make_elim elim_rls rl =
-      standard (tryres (rl, elim_rls @ [revcut_rl]));
+      Drule.standard (tryres (rl, elim_rls @ [revcut_rl]));
 
 (*Turns iff rules into safe elimination rules*)
 fun mk_free_SEs iffs = map (gen_make_elim [@{thm conjE}, @{thm FalseE}]) (iffs RL [@{thm iffD1}]);