src/FOL/simpdata.ML

--- a/src/FOL/simpdata.ML	Fri Oct 16 10:55:07 2009 +0200
+++ b/src/FOL/simpdata.ML	Sat Oct 17 00:52:37 2009 +0200
@@ -27,7 +27,7 @@
 
 (*Congruence rules for = or <-> (instead of ==)*)
 fun mk_meta_cong rl =
-  standard(mk_meta_eq (mk_meta_prems rl))
+  Drule.standard (mk_meta_eq (mk_meta_prems rl))
   handle THM _ =>
   error("Premises and conclusion of congruence rules must use =-equality or <->");