# 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