diff -r c39860141415 -r 675c0c7e6a37 src/Sequents/simpdata.ML
--- a/src/Sequents/simpdata.ML	Fri Oct 16 10:55:07 2009 +0200
+++ b/src/Sequents/simpdata.ML	Sat Oct 17 00:52:37 2009 +0200
@@ -49,7 +49,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 <->");