# HG changeset patch
# User wenzelm
# Date 1192622138 -7200
# Node ID a11d25316c3db1ce925c7b0f2871131fc443fc87
# Parent  0f19e65ac0b6237c034bdf5be54d54acb2727d70
tuned fork_mixfix (back from class.ML);

diff -r 0f19e65ac0b6 -r a11d25316c3d src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Wed Oct 17 13:55:37 2007 +0200
+++ b/src/Pure/Isar/theory_target.ML	Wed Oct 17 13:55:38 2007 +0200
@@ -161,6 +161,10 @@
 
 (* consts *)
 
+fun fork_mixfix false _ mx = (NoSyn, NoSyn, mx)
+  | fork_mixfix true false mx = (NoSyn, mx, NoSyn)
+  | fork_mixfix true true mx = (mx, NoSyn, NoSyn);
+
 fun locale_const (prmode as (mode, _)) pos ((c, mx), rhs) phi =
   let
     val c' = Morphism.name phi c;
@@ -186,7 +190,7 @@
     fun const ((c, T), mx) thy =
       let
         val U = map #2 xs ---> T;
-        val ((mx1, mx2), mx3) = Class.fork_mixfix is_locale is_class mx;
+        val (mx1, mx2, mx3) = fork_mixfix is_locale is_class mx;
         val (const, thy') = Sign.declare_const pos (c, U, mx3) thy;
         val t = Term.list_comb (const, map Free xs);
       in (((c, mx2), t), thy') end;
@@ -228,8 +232,8 @@
     val c = Morphism.name target_morphism raw_c;
     val t = Morphism.term target_morphism raw_t;
 
-    val xs = map Free (Variable.add_fixed target_ctxt t []);
-    val ((mx1, mx2), mx3) = Class.fork_mixfix is_locale is_class mx;
+    val xs = map Free (rev (Variable.add_fixed target_ctxt t []));
+    val (mx1, mx2, mx3) = fork_mixfix is_locale is_class mx;
 
     val global_rhs =
       singleton (Variable.export_terms (Variable.declare_term t target_ctxt) thy_ctxt)