clarified fork_mixfix
authorhaftmann
Tue Oct 16 23:12:58 2007 +0200 (2007-10-16)
changeset 25064c6664770ef6c
parent 25063 8e702c7adc34
child 25065 25696ce6dff1
clarified fork_mixfix
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/theory_target.ML	Tue Oct 16 23:12:57 2007 +0200
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Tue Oct 16 23:12:58 2007 +0200
     1.3 @@ -186,15 +186,13 @@
     1.4      fun const ((c, T), mx) thy =
     1.5        let
     1.6          val U = map #2 xs ---> T;
     1.7 -        val (mx1, mx2) = Class.fork_mixfix is_locale is_class mx;
     1.8 -        val mx3 = if is_locale then NoSyn else mx1;
     1.9 +        val ((mx1, mx2), mx3) = Class.fork_mixfix is_locale is_class mx;
    1.10          val (const, thy') = Sign.declare_const pos (c, U, mx3) thy;
    1.11          val t = Term.list_comb (const, map Free xs);
    1.12        in (((c, mx2), t), thy') end;
    1.13 -    val local_const = NameSpace.full (LocalTheory.target_naming lthy);
    1.14      fun class_const ((c, _), mx) (_, t) =
    1.15 -      LocalTheory.raw_theory_result (Class.add_const_in_class target ((c, mx), (local_const c, t)))
    1.16 -      #-> Class.remove_constraint target;
    1.17 +      LocalTheory.raw_theory_result (Class.add_const_in_class target ((c, mx), t))
    1.18 +      #-> LocalTheory.target o Class.remove_constraint target;
    1.19  
    1.20      val (abbrs, lthy') = lthy
    1.21        |> LocalTheory.theory_result (fold_map const decls)
    1.22 @@ -216,8 +214,8 @@
    1.23  
    1.24  fun class_abbrev target prmode ((c, mx), rhs) lthy = lthy   (* FIXME pos *)
    1.25    |> LocalTheory.raw_theory_result (Class.add_abbrev_in_class target prmode
    1.26 -      ((c, mx), (NameSpace.full (LocalTheory.target_naming lthy) c, rhs)))
    1.27 -  |-> Class.remove_constraint target;
    1.28 +      ((c, mx), rhs))
    1.29 +  |-> LocalTheory.target o Class.remove_constraint target;
    1.30  
    1.31  in
    1.32  
    1.33 @@ -230,11 +228,12 @@
    1.34      val c = Morphism.name target_morphism raw_c;
    1.35      val t = Morphism.term target_morphism raw_t;
    1.36  
    1.37 -    val xs = map Free (rev (Variable.add_fixed target_ctxt t []));
    1.38 +    val xs = map Free (Variable.add_fixed target_ctxt t []);
    1.39 +    val ((mx1, mx2), mx3) = Class.fork_mixfix is_locale is_class mx;
    1.40 +
    1.41      val global_rhs =
    1.42        singleton (Variable.export_terms (Variable.declare_term t target_ctxt) thy_ctxt)
    1.43          (fold_rev lambda xs t);
    1.44 -    val (mx1, mx2) = Class.fork_mixfix is_locale is_class mx;
    1.45    in
    1.46      if is_locale then
    1.47        lthy
    1.48 @@ -249,7 +248,7 @@
    1.49        lthy
    1.50        |> LocalTheory.theory
    1.51          (Sign.add_abbrev (#1 prmode) pos (c, global_rhs)
    1.52 -          #-> (fn (lhs, _) => Sign.notation true prmode [(lhs, mx1)]))
    1.53 +          #-> (fn (lhs, _) => Sign.notation true prmode [(lhs, mx3)]))
    1.54        |> context_abbrev pos (c, raw_t)
    1.55    end;
    1.56