--- a/src/Sequents/simpdata.ML Fri Apr 30 17:18:29 2010 +0200
+++ b/src/Sequents/simpdata.ML Fri Apr 30 18:06:29 2010 +0200
@@ -42,13 +42,13 @@
Display.string_of_thm_without_context th));
(*Replace premises x=y, X<->Y by X==Y*)
-val mk_meta_prems =
- rule_by_tactic
+fun mk_meta_prems ctxt =
+ rule_by_tactic ctxt
(REPEAT_FIRST (resolve_tac [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}]));
(*Congruence rules for = or <-> (instead of ==)*)
-fun mk_meta_cong (_: simpset) rl =
- Drule.export_without_context(mk_meta_eq (mk_meta_prems rl))
+fun mk_meta_cong ss rl =
+ Drule.export_without_context (mk_meta_eq (mk_meta_prems (Simplifier.the_context ss) rl))
handle THM _ =>
error("Premises and conclusion of congruence rules must use =-equality or <->");