--- 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;
--- 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)