tuned
authorhaftmann
Mon Oct 15 15:29:46 2007 +0200 (2007-10-15)
changeset 250404e54c5ae6852
parent 25039 06ed511837d5
child 25041 c1efae25ee76
tuned
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/theory_target.ML	Mon Oct 15 15:29:45 2007 +0200
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Mon Oct 15 15:29:46 2007 +0200
     1.3 @@ -38,7 +38,6 @@
     1.4    let
     1.5      val thy = ProofContext.theory_of ctxt;
     1.6      val target_name = (if is_class then "class " else "locale ") ^ Locale.extern thy target;
     1.7 -
     1.8      val fixes = map (fn (x, T) => (x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt));
     1.9      val assumes = map (fn A => (("", []), [(A, [])])) (map Thm.term_of (Assumption.assms_of ctxt));
    1.10      val elems =
    1.11 @@ -199,16 +198,17 @@
    1.12          val (const, thy') = Sign.declare_const (ContextPosition.properties_of lthy) (c, U, mx3) thy;
    1.13          val t = Term.list_comb (const, map Free xs);
    1.14        in (((c, mx2), t), thy') end;
    1.15 -    fun const_class ((c, _), mx) (_, t) =
    1.16 -      LocalTheory.raw_theory_result (Class.add_const_in_class target ((c, mx), t))
    1.17 +    val local_const = NameSpace.full (LocalTheory.target_naming lthy);
    1.18 +    fun class_const ((c, _), mx) (_, t) =
    1.19 +      LocalTheory.raw_theory_result (Class.add_const_in_class target ((c, mx), (local_const c, t)))
    1.20        #-> Class.remove_constraint target;
    1.21  
    1.22      val (abbrs, lthy') = lthy
    1.23        |> LocalTheory.theory_result (fold_map const decls)
    1.24    in
    1.25      lthy'
    1.26 -    |> is_class ? fold2 const_class decls abbrs
    1.27      |> is_locale ? fold (internal_abbrev ta Syntax.mode_default) abbrs
    1.28 +    |> is_class ? fold2 class_const decls abbrs
    1.29      |> fold_map (apfst (apsnd snd) oo LocalDefs.add_def) abbrs
    1.30    end;
    1.31  
    1.32 @@ -227,12 +227,14 @@
    1.33      val xs = map Free (Variable.add_fixed target_ctxt t []);
    1.34      val u = fold_rev lambda xs t;
    1.35      val U = Term.fastype_of u;
    1.36 -
    1.37      val u' = singleton (Variable.export_terms (Variable.declare_term u target_ctxt) thy_ctxt) u;
    1.38      val (mx1, mx2) = Class.fork_mixfix is_locale is_class mx;
    1.39      val mx3 = if is_locale then NoSyn else mx1;
    1.40 -    fun add_abbrev_in_class abbr =
    1.41 -      LocalTheory.raw_theory_result (Class.add_abbrev_in_class target prmode abbr)
    1.42 +
    1.43 +    val local_const = NameSpace.full (LocalTheory.target_naming lthy);
    1.44 +    fun class_abbrev ((c, mx), t) =
    1.45 +      LocalTheory.raw_theory_result (Class.add_abbrev_in_class target prmode
    1.46 +        ((c, mx), (local_const c, t)))
    1.47        #-> Class.remove_constraint target;
    1.48    in
    1.49      lthy
    1.50 @@ -241,7 +243,7 @@
    1.51      |-> (fn (lhs, rhs) =>
    1.52            LocalTheory.theory (Sign.notation true prmode [(lhs, mx3)])
    1.53            #> is_locale ? internal_abbrev ta prmode ((c, mx2), Term.list_comb (lhs, xs))
    1.54 -          #> is_class ? add_abbrev_in_class ((c, mx1), Term.list_comb (lhs, xs)))
    1.55 +          #> is_class ? class_abbrev ((c, mx1), Term.list_comb (lhs, xs)))
    1.56      |> LocalDefs.add_def ((c, NoSyn), raw_t)
    1.57    end;
    1.58