--- a/src/Sequents/simpdata.ML Sun Feb 07 19:31:55 2010 +0100
+++ b/src/Sequents/simpdata.ML Sun Feb 07 19:33:34 2010 +0100
@@ -49,9 +49,9 @@
(*Congruence rules for = or <-> (instead of ==)*)
fun mk_meta_cong rl =
- Drule.standard(mk_meta_eq (mk_meta_prems rl))
- handle THM _ =>
- error("Premises and conclusion of congruence rules must use =-equality or <->");
+ Drule.export_without_context(mk_meta_eq (mk_meta_prems rl))
+ handle THM _ =>
+ error("Premises and conclusion of congruence rules must use =-equality or <->");
(*** Standard simpsets ***)