# HG changeset patch
# User wenzelm
# Date 1459368055 -7200
# Node ID dd2914250ca721fb6b6e18ee8a4b4223da87f443
# Parent  6e6cacf8fe504cd83b27da4a9f64f3e4528dfc60
more accurate mixfix type constraints;

diff -r 6e6cacf8fe50 -r dd2914250ca7 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Mar 30 21:34:00 2016 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Mar 30 22:00:55 2016 +0200
@@ -594,21 +594,25 @@
 
 local
 
+fun read_arg (c, mx) ctxt =
+  (case Proof_Context.read_const {proper = false, strict = false} ctxt c of
+    Free (x, _) =>
+      let
+        val ctxt' =
+          ctxt |> is_none (Variable.default_type ctxt x) ?
+            Variable.declare_constraints (Free (x, Mixfix.mixfixT mx));
+        val t = Free (#1 (Proof_Context.inferred_param x ctxt'));
+      in ((t, mx), ctxt') end
+  | t => ((t, mx), ctxt));
+
 fun gen_write prep_arg mode args =
   assert_forward
-  #> map_context (fn ctxt => ctxt |> Proof_Context.notation true mode (map (prep_arg ctxt) args))
+  #> map_context (fold_map prep_arg args #-> Proof_Context.notation true mode)
   #> reset_facts;
 
-fun read_arg ctxt (c, mx) =
-  (case Proof_Context.read_const {proper = false, strict = false} ctxt c of
-    Free (x, _) =>
-      let val T = Proof_Context.infer_type ctxt (x, Mixfix.mixfixT mx)
-      in (Free (x, T), mx) end
-  | t => (t, mx));
-
 in
 
-val write = gen_write (K I);
+val write = gen_write pair;
 val write_cmd = gen_write read_arg;
 
 end;
diff -r 6e6cacf8fe50 -r dd2914250ca7 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Wed Mar 30 21:34:00 2016 +0200
+++ b/src/Pure/variable.ML	Wed Mar 30 22:00:55 2016 +0200
@@ -230,6 +230,9 @@
 
 (* constraints *)
 
+fun constrain_var (xi, T) =
+  if T = dummyT then Vartab.delete_safe xi else Vartab.update (xi, T);
+
 fun constrain_tvar (xi, raw_S) =
   let val S = #2 (Term_Position.decode_positionS raw_S)
   in if S = dummyS then Vartab.delete_safe xi else Vartab.update (xi, S) end;
@@ -237,8 +240,8 @@
 fun declare_constraints t = map_constraints (fn (types, sorts) =>
   let
     val types' = fold_aterms
-      (fn Free (x, T) => Vartab.update ((x, ~1), T)
-        | Var v => Vartab.update v
+      (fn Free (x, T) => constrain_var ((x, ~1), T)
+        | Var v => constrain_var v
         | _ => I) t types;
     val sorts' = (fold_types o fold_atyps)
       (fn TFree (x, S) => constrain_tvar ((x, ~1), S)