# HG changeset patch
# User haftmann
# Date 1232177380 -3600
# Node ID ad7991d7b5bbc3a956e86030e6e60a5e7a75300e
# Parent  941ad06c7f9c4780db8c766de75e24158bcc34ad
explicit equation morphism

diff -r 941ad06c7f9c -r ad7991d7b5bb src/Pure/Isar/element.ML
--- 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;
diff -r 941ad06c7f9c -r ad7991d7b5bb src/Pure/Isar/expression.ML
--- 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