src/Sequents/simpdata.ML
changeset 32957 675c0c7e6a37
parent 32155 e2bf2f73b0c8
child 35021 c839a4c670c6
--- 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 <->");