--- a/src/Pure/Isar/element.ML Sat Jan 17 08:29:19 2009 +0100
+++ b/src/Pure/Isar/element.ML Sat Jan 17 08:29:40 2009 +0100
@@ -78,6 +78,7 @@
val generalize_facts: Proof.context -> Proof.context ->
(Attrib.binding * (thm list * Attrib.src list) list) list ->
(Attrib.binding * (thm list * Attrib.src list) list) list
+ val eq_morphism: theory -> thm list -> morphism
val transfer_morphism: theory -> morphism
val activate: (typ, term, Facts.ref) ctxt list -> Proof.context -> context_i list * Proof.context
val activate_i: context_i list -> Proof.context -> context_i list * Proof.context
@@ -521,6 +522,14 @@
fun satisfy_facts witns = facts_map (morph_ctxt (satisfy_morphism witns));
+(* rewriting with equalities *)
+
+fun eq_morphism thy thms = Morphism.morphism
+ {binding = I, var = I, typ = I,
+ term = MetaSimplifier.rewrite_term thy thms [],
+ fact = map (MetaSimplifier.rewrite_rule thms)};
+
+
(* generalize type/term parameters *)
val maxidx_atts = fold Args.maxidx_values;