tuned;
authorwenzelm
Mon Oct 22 21:32:12 2007 +0200 (2007-10-22)
changeset 251509d8893e9f381
parent 25149 776f985efa4c
child 25151 9374a0df240c
tuned;
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/theory_target.ML	Mon Oct 22 21:32:09 2007 +0200
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Mon Oct 22 21:32:12 2007 +0200
     1.3 @@ -215,7 +215,6 @@
     1.4      val u = fold_rev lambda xs t';
     1.5      val global_rhs =
     1.6        singleton (Variable.export_terms (Variable.declare_term u target_ctxt) thy_ctxt) u;
     1.7 -    val class_t = Morphism.term (LocalTheory.target_morphism lthy) t;
     1.8    in
     1.9      lthy |>
    1.10       (if is_locale then
    1.11 @@ -223,8 +222,7 @@
    1.12          #-> (fn (lhs, _) =>
    1.13            let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
    1.14              term_syntax ta (locale_const prmode pos ((c, mx2), lhs')) #>
    1.15 -            is_class ?
    1.16 -              class_target ta (Class.add_syntactic_const target prmode pos ((c, mx1), class_t))
    1.17 +            is_class ? class_target ta (Class.add_syntactic_const target prmode pos ((c, mx1), t'))
    1.18            end)
    1.19        else
    1.20          LocalTheory.theory