# HG changeset patch
# User wenzelm
# Date 1459364199 -7200
# Node ID d6b0d35b3aed1355e3a9ce84fc940df4e456ba12
# Parent  70b73465f636230d0321f1ead4673fb1aec9308b
relevant check_mixfix happens further at the bottom, to avoid duplicate reports via Specification.prepare;

diff -r 70b73465f636 -r d6b0d35b3aed src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Wed Mar 30 20:35:35 2016 +0200
+++ b/src/Pure/Isar/generic_target.ML	Wed Mar 30 20:56:39 2016 +0200
@@ -98,30 +98,21 @@
   in (global_rhs, (extra_tfrees, (type_params, term_params))) end;
 
 fun check_mixfix ctxt (b, extra_tfrees) mx =
-  let
-    val visible = Context_Position.is_visible ctxt;
-    val _ =
-      ctxt |> Proof_Context.add_fixes
-        [(Binding.reset_pos b, NONE, if visible then mx else Mixfix.reset_pos mx)];
-    val mx' =
-      if null extra_tfrees then mx
-      else
-       (if visible then
-          warning
-            ("Additional type variable(s) in specification of " ^ Binding.print b ^ ": " ^
-              commas (map (Syntax.string_of_typ ctxt o TFree) (sort_by #1 extra_tfrees)) ^
-              (if Mixfix.is_empty mx then ""
-               else
-                "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx) ^
-                  Position.here (Mixfix.pos_of mx)))
-        else (); NoSyn);
-  in Mixfix.reset_pos mx' end;
+  if null extra_tfrees then mx
+  else
+   (if Context_Position.is_visible ctxt then
+      warning
+        ("Additional type variable(s) in specification of " ^ Binding.print b ^ ": " ^
+          commas (map (Syntax.string_of_typ ctxt o TFree) (sort_by #1 extra_tfrees)) ^
+          (if Mixfix.is_empty mx then ""
+           else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx)))
+    else (); NoSyn);
 
 fun check_mixfix_global (b, no_params) mx =
   if no_params orelse Mixfix.is_empty mx then mx
   else
     (warning ("Dropping global mixfix syntax: " ^ Binding.print b ^ " " ^
-      Pretty.string_of (Mixfix.pretty_mixfix mx) ^ Position.here (Mixfix.pos_of mx)); NoSyn);
+      Pretty.string_of (Mixfix.pretty_mixfix mx)); NoSyn);
 
 fun same_const (Const (c, _), Const (c', _)) = c = c'
   | same_const (t $ _, t' $ _) = same_const (t, t')
diff -r 70b73465f636 -r d6b0d35b3aed src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Mar 30 20:35:35 2016 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Mar 30 20:56:39 2016 +0200
@@ -1062,6 +1062,9 @@
   let val T = (case opt_T of SOME T => T | NONE => Mixfix.mixfixT mx)
   in ((x, T, mx), ctxt |> Variable.declare_constraints (Free (x, T))) end;
 
+fun add_syntax vars ctxt =
+  map_syntax_idents (Local_Syntax.add_syntax ctxt (map (pair Local_Syntax.Fixed) vars)) ctxt;
+
 fun check_var internal b =
   let
     val x = Variable.check_name b;
@@ -1073,6 +1076,14 @@
 
 local
 
+fun check_mixfix ctxt (b, opt_T, mx) =
+  let
+    val ([x], ctxt') = Variable.add_fixes_binding [Binding.reset_pos b] ctxt;
+    val mx' = Mixfix.reset_pos mx;
+    val T = #2 (#1 (declare_var (x, opt_T, mx') ctxt));
+    val _ = add_syntax [(x, T, if Context_Position.is_visible ctxt then mx else mx')] ctxt';
+  in mx' end;
+
 fun prep_var prep_typ internal (b, raw_T, mx) ctxt =
   let
     val x = check_var internal b;
@@ -1080,8 +1091,9 @@
       if internal then T
       else Type.no_tvars T handle TYPE (msg, _, _) => error msg;
     val opt_T = Option.map (cond_tvars o prep_typ ctxt) raw_T;
-    val (_, ctxt') = ctxt |> declare_var (x, opt_T, mx);
-  in ((b, opt_T, mx), ctxt') end;
+    val mx' = if Mixfix.is_empty mx then mx else check_mixfix ctxt (b, opt_T, mx);
+    val (_, ctxt') = ctxt |> declare_var (x, opt_T, mx');
+  in ((b, opt_T, mx'), ctxt') end;
 
 in
 
@@ -1185,7 +1197,7 @@
   in
     ctxt'
     |> fold_map declare_var (map2 (fn x => fn (_, T, mx) => (x, T, mx)) xs vars)
-    |-> (map_syntax_idents o Local_Syntax.add_syntax ctxt o map (pair Local_Syntax.Fixed))
+    |-> add_syntax
     |> pair xs
   end;