1.1 --- a/src/Pure/Isar/theory_target.ML	Thu Oct 18 09:20:58 2007 +0200
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Thu Oct 18 09:20:59 2007 +0200
     1.3 @@ -161,9 +161,9 @@
     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 +fun fork_mixfix false _ mx = ((NoSyn, NoSyn), mx)
    1.11 +  | fork_mixfix true false mx = ((NoSyn, mx), NoSyn)
    1.12 +  | fork_mixfix true true mx = ((mx, NoSyn), NoSyn);
    1.13  
    1.14  fun locale_const (prmode as (mode, _)) pos ((c, mx), rhs) phi =
    1.15    let
    1.16 @@ -190,21 +190,22 @@
    1.17      fun const ((c, T), mx) thy =
    1.18        let
    1.19          val U = map #2 xs ---> T;
    1.20 -        val (mx1, mx2, mx3) = fork_mixfix is_locale is_class mx;
    1.21 +        val (mx12, mx3) = fork_mixfix is_locale is_class mx;
    1.22          val (const, thy') = Sign.declare_const pos (c, U, mx3) thy;
    1.23          val t = Term.list_comb (const, map Free xs);
    1.24 -      in (((c, mx2), t), thy') end;
    1.25 -    fun class_const ((c, _), mx) (_, t) =
    1.26 -      LocalTheory.raw_theory_result (Class.add_const_in_class target ((c, mx), t))
    1.27 +      in (((c, mx12), t), thy') end;
    1.28 +    fun class_const ((c, _), _) ((_, (mx1, _)), t) =
    1.29 +      LocalTheory.raw_theory_result (Class.add_const_in_class target ((c, mx1), t))
    1.30        #-> LocalTheory.target o Class.remove_constraint target;
    1.31  
    1.32      val (abbrs, lthy') = lthy
    1.33        |> LocalTheory.theory_result (fold_map const decls)
    1.34 +    val abbrs' = (map o apfst o apsnd) snd abbrs;
    1.35    in
    1.36      lthy'
    1.37 -    |> is_locale ? fold (term_syntax ta o locale_const Syntax.mode_default pos) abbrs
    1.38 +    |> is_locale ? fold (term_syntax ta o locale_const Syntax.mode_default pos) abbrs'
    1.39      |> is_class ? fold2 class_const decls abbrs
    1.40 -    |> fold_map (apfst (apsnd snd) oo LocalDefs.add_def) abbrs
    1.41 +    |> fold_map (apfst (apsnd snd) oo LocalDefs.add_def) abbrs'
    1.42    end;
    1.43  
    1.44  
    1.45 @@ -233,7 +234,7 @@
    1.46      val t = Morphism.term target_morphism raw_t;
    1.47  
    1.48      val xs = map Free (rev (Variable.add_fixed target_ctxt t []));
    1.49 -    val (mx1, mx2, mx3) = fork_mixfix is_locale is_class mx;
    1.50 +    val ((mx1, mx2), mx3) = fork_mixfix is_locale is_class mx;
    1.51  
    1.52      val global_rhs =
    1.53        singleton (Variable.export_terms (Variable.declare_term t target_ctxt) thy_ctxt)