equal
deleted
inserted
replaced
73 |
73 |
74 fun infer_type sg (env as Envir.Envir {maxidx, asol, iTs}) Ts vTs |
74 fun infer_type sg (env as Envir.Envir {maxidx, asol, iTs}) Ts vTs |
75 (t as Const (s, T)) = if T = dummyT then (case Sign.const_type sg s of |
75 (t as Const (s, T)) = if T = dummyT then (case Sign.const_type sg s of |
76 NONE => error ("reconstruct_proof: No such constant: " ^ quote s) |
76 NONE => error ("reconstruct_proof: No such constant: " ^ quote s) |
77 | SOME T => |
77 | SOME T => |
78 let val T' = incr_tvar (maxidx + 1) T |
78 let val T' = Logic.incr_tvar (maxidx + 1) T |
79 in (Const (s, T'), T', vTs, |
79 in (Const (s, T'), T', vTs, |
80 Envir.Envir {maxidx = maxidx + 1, asol = asol, iTs = iTs}) |
80 Envir.Envir {maxidx = maxidx + 1, asol = asol, iTs = iTs}) |
81 end) |
81 end) |
82 else (t, T, vTs, env) |
82 else (t, T, vTs, env) |
83 | infer_type sg env Ts vTs (t as Free (s, T)) = |
83 | infer_type sg env Ts vTs (t as Free (s, T)) = |
353 (fn (b, NONE) => a = b |
353 (fn (b, NONE) => a = b |
354 | (b, SOME prop') => a = b andalso prop = prop') thms) |
354 | (b, SOME prop') => a = b andalso prop = prop') thms) |
355 then (maxidx, prfs, prf) else |
355 then (maxidx, prfs, prf) else |
356 let |
356 let |
357 fun inc i = |
357 fun inc i = |
358 map_proof_terms (Logic.incr_indexes ([], i)) (incr_tvar i); |
358 map_proof_terms (Logic.incr_indexes ([], i)) (Logic.incr_tvar i); |
359 val (maxidx', prf, prfs') = |
359 val (maxidx', prf, prfs') = |
360 (case gen_assoc (op =) (prfs, (a, prop)) of |
360 (case gen_assoc (op =) (prfs, (a, prop)) of |
361 NONE => |
361 NONE => |
362 let |
362 let |
363 val _ = message ("Reconstructing proof of " ^ a); |
363 val _ = message ("Reconstructing proof of " ^ a); |