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 <->");