# HG changeset patch # User haftmann # Date 1192454986 -7200 # Node ID 4e54c5ae68529f6cccd1d5608e241ee2d5ef665d # Parent 06ed511837d515345a6a93c3a0f9924eb78eca74 tuned diff -r 06ed511837d5 -r 4e54c5ae6852 src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Mon Oct 15 15:29:45 2007 +0200 +++ b/src/Pure/Isar/theory_target.ML Mon Oct 15 15:29:46 2007 +0200 @@ -38,7 +38,6 @@ let val thy = ProofContext.theory_of ctxt; val target_name = (if is_class then "class " else "locale ") ^ Locale.extern thy target; - val fixes = map (fn (x, T) => (x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt)); val assumes = map (fn A => (("", []), [(A, [])])) (map Thm.term_of (Assumption.assms_of ctxt)); val elems = @@ -199,16 +198,17 @@ val (const, thy') = Sign.declare_const (ContextPosition.properties_of lthy) (c, U, mx3) thy; val t = Term.list_comb (const, map Free xs); in (((c, mx2), t), thy') end; - fun const_class ((c, _), mx) (_, t) = - LocalTheory.raw_theory_result (Class.add_const_in_class target ((c, mx), t)) + val local_const = NameSpace.full (LocalTheory.target_naming lthy); + fun class_const ((c, _), mx) (_, t) = + LocalTheory.raw_theory_result (Class.add_const_in_class target ((c, mx), (local_const c, t))) #-> Class.remove_constraint target; val (abbrs, lthy') = lthy |> LocalTheory.theory_result (fold_map const decls) in lthy' - |> is_class ? fold2 const_class decls abbrs |> is_locale ? fold (internal_abbrev ta Syntax.mode_default) abbrs + |> is_class ? fold2 class_const decls abbrs |> fold_map (apfst (apsnd snd) oo LocalDefs.add_def) abbrs end; @@ -227,12 +227,14 @@ val xs = map Free (Variable.add_fixed target_ctxt t []); val u = fold_rev lambda xs t; val U = Term.fastype_of u; - val u' = singleton (Variable.export_terms (Variable.declare_term u target_ctxt) thy_ctxt) u; val (mx1, mx2) = Class.fork_mixfix is_locale is_class mx; val mx3 = if is_locale then NoSyn else mx1; - fun add_abbrev_in_class abbr = - LocalTheory.raw_theory_result (Class.add_abbrev_in_class target prmode abbr) + + val local_const = NameSpace.full (LocalTheory.target_naming lthy); + fun class_abbrev ((c, mx), t) = + LocalTheory.raw_theory_result (Class.add_abbrev_in_class target prmode + ((c, mx), (local_const c, t))) #-> Class.remove_constraint target; in lthy @@ -241,7 +243,7 @@ |-> (fn (lhs, rhs) => LocalTheory.theory (Sign.notation true prmode [(lhs, mx3)]) #> is_locale ? internal_abbrev ta prmode ((c, mx2), Term.list_comb (lhs, xs)) - #> is_class ? add_abbrev_in_class ((c, mx1), Term.list_comb (lhs, xs))) + #> is_class ? class_abbrev ((c, mx1), Term.list_comb (lhs, xs))) |> LocalDefs.add_def ((c, NoSyn), raw_t) end;