src/HOL/Tools/SMT/z3_proof_reconstruction.ML

       | SOME (Proved p) => (p, cxp)
       | NONE => z3_exn ("unknown proof id: " ^ quote (string_of_int idx)))
 
     fun result (p, (cx, _)) = (thm_of p, cx)
   in
-    (fn (idx, ptab) => result (lookup idx (ctxt, Inttab.map Unproved ptab)))
+    (fn (idx, ptab) => result (lookup idx (ctxt, Inttab.map (K Unproved) ptab)))
   end
 
 fun reconstruct (output, {typs, terms, unfolds, assms}) ctxt =
   P.parse ctxt typs terms output
   |> (fn (idx, (ptab, vars, cx)) => prove cx unfolds assms vars (idx, ptab))