# HG changeset patch
# User wenzelm
# Date 1165786023 -3600
# Node ID d4fd9bb0ccd63c96b33adbfd1f54460eeaa8ab2a
# Parent  78248dda3a9009fb7d29c96fbe2a0245d266517b
defs: increased entropy of mixfix handling;

diff -r 78248dda3a90 -r d4fd9bb0ccd6 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Sun Dec 10 20:09:08 2006 +0100
+++ b/src/Pure/Isar/theory_target.ML	Sun Dec 10 22:27:03 2006 +0100
@@ -86,7 +86,7 @@
       |> LocalTheory.theory_result (Sign.add_abbrev (#1 prmode) (c, u'));
     val v = Const (#1 const, Term.fastype_of u);
     val v' = Const const;
-    (* FIXME !? *)
+    (* FIXME proper handling of mixfix !? *)
     val mx' = if is_class lthy then NoSyn else Syntax.unlocalize_mixfix is_loc mx;
   in
     lthy1
@@ -105,13 +105,14 @@
       let
         val U = map #2 xs ---> T;
         val t = Term.list_comb (Const (Sign.full_name thy c, U), map Free xs);
-        (* FIXME !? *)
+        (* FIXME proper handling of mixfix !? *)
         val mx' = if is_class lthy then NoSyn else Syntax.unlocalize_mixfix is_loc mx;
         val thy' = Sign.add_consts_authentic [(c, U, mx')] thy;
       in (((c, mx), t), thy') end;
 
     val (abbrs, lthy') = lthy |> LocalTheory.theory_result (fold_map const decls);
-    val defs = abbrs |> map (fn (x, t) => (x, (("", []), t)));
+    val defs = abbrs    (* FIXME proper handling of mixfix !? *)
+      |> map (fn ((c, mx), t) => ((c, if is_loc then mx else NoSyn), (("", []), t)));
   in
     lthy'
     |> is_loc ? fold internal_abbrev abbrs