src/Pure/Isar/proof_context.ML

 
 fun declare_var (x, opt_T, mx) ctxt =
   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;
     val check = if internal then Name.reject_skolem else Name.reject_internal;
     val _ =

       else error ("Bad name: " ^ Binding.print b);
   in x end;
 
 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;
     fun cond_tvars T =
       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
 
 val read_var = prep_var Syntax.read_typ false;
 val cert_var = prep_var cert_typ true;

     val (vars, _) = fold_map prep_var raw_vars ctxt;
     val (xs, ctxt') = Variable.add_fixes_binding (map #1 vars) ctxt;
   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;
 
 in