# HG changeset patch
# User wenzelm
# Date 1193081532 -7200
# Node ID 9d8893e9f381fe455023587ba2c6b7fb07e38b51
# Parent  776f985efa4c54d7ed5cff723fbecc76adb8a958
tuned;

diff -r 776f985efa4c -r 9d8893e9f381 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Mon Oct 22 21:32:09 2007 +0200
+++ b/src/Pure/Isar/theory_target.ML	Mon Oct 22 21:32:12 2007 +0200
@@ -215,7 +215,6 @@
     val u = fold_rev lambda xs t';
     val global_rhs =
       singleton (Variable.export_terms (Variable.declare_term u target_ctxt) thy_ctxt) u;
-    val class_t = Morphism.term (LocalTheory.target_morphism lthy) t;
   in
     lthy |>
      (if is_locale then
@@ -223,8 +222,7 @@
         #-> (fn (lhs, _) =>
           let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
             term_syntax ta (locale_const prmode pos ((c, mx2), lhs')) #>
-            is_class ?
-              class_target ta (Class.add_syntactic_const target prmode pos ((c, mx1), class_t))
+            is_class ? class_target ta (Class.add_syntactic_const target prmode pos ((c, mx1), t'))
           end)
       else
         LocalTheory.theory