explicit equation morphism

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

--- a/src/Pure/Isar/expression.ML	Sat Jan 17 08:29:19 2009 +0100
+++ b/src/Pure/Isar/expression.ML	Sat Jan 17 08:29:40 2009 +0100
@@ -865,9 +865,7 @@
               Morphism.thm (export' $> export) #>
               LocalDefs.meta_rewrite_rule (ProofContext.init thy) #>
               Drule.abs_def);
-            val eq_morph =
-              Morphism.term_morphism (MetaSimplifier.rewrite_term thy thms' []) $>
-              Morphism.thm_morphism (MetaSimplifier.rewrite_rule thms');
+            val eq_morph = Element.eq_morphism thy thms';
             val eq_attns' = map ((apsnd o map) (Attrib.attribute_i thy)) eq_attns;
           in
             thy