src/Pure/Isar/theory_target.ML
changeset 25068 a11d25316c3d
parent 25064 c6664770ef6c
child 25079 db5fdc34f3af
     1.1 --- a/src/Pure/Isar/theory_target.ML	Wed Oct 17 13:55:37 2007 +0200
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Wed Oct 17 13:55:38 2007 +0200
     1.3 @@ -161,6 +161,10 @@
     1.4  
     1.5  (* consts *)
     1.6  
     1.7 +fun fork_mixfix false _ mx = (NoSyn, NoSyn, mx)
     1.8 +  | fork_mixfix true false mx = (NoSyn, mx, NoSyn)
     1.9 +  | fork_mixfix true true mx = (mx, NoSyn, NoSyn);
    1.10 +
    1.11  fun locale_const (prmode as (mode, _)) pos ((c, mx), rhs) phi =
    1.12    let
    1.13      val c' = Morphism.name phi c;
    1.14 @@ -186,7 +190,7 @@
    1.15      fun const ((c, T), mx) thy =
    1.16        let
    1.17          val U = map #2 xs ---> T;
    1.18 -        val ((mx1, mx2), mx3) = Class.fork_mixfix is_locale is_class mx;
    1.19 +        val (mx1, mx2, mx3) = fork_mixfix is_locale is_class mx;
    1.20          val (const, thy') = Sign.declare_const pos (c, U, mx3) thy;
    1.21          val t = Term.list_comb (const, map Free xs);
    1.22        in (((c, mx2), t), thy') end;
    1.23 @@ -228,8 +232,8 @@
    1.24      val c = Morphism.name target_morphism raw_c;
    1.25      val t = Morphism.term target_morphism raw_t;
    1.26  
    1.27 -    val xs = map Free (Variable.add_fixed target_ctxt t []);
    1.28 -    val ((mx1, mx2), mx3) = Class.fork_mixfix is_locale is_class mx;
    1.29 +    val xs = map Free (rev (Variable.add_fixed target_ctxt t []));
    1.30 +    val (mx1, mx2, mx3) = fork_mixfix is_locale is_class mx;
    1.31  
    1.32      val global_rhs =
    1.33        singleton (Variable.export_terms (Variable.declare_term t target_ctxt) thy_ctxt)