--- a/src/Pure/Proof/extraction.ML Mon Jul 29 10:26:12 2019 +0200
+++ b/src/Pure/Proof/extraction.ML Mon Jul 29 11:09:37 2019 +0200
@@ -365,7 +365,7 @@
fun abs_corr_shyps thy thm vs xs prf =
let
val S = Sign.defaultS thy;
- val {atyp_map, constraints, prop = prop', ...} =
+ val (ucontext, prop') =
Logic.unconstrainT (Thm.shyps_of thm) (Thm.prop_of thm);
val atyps = fold_types (fold_atyps (insert (op =))) (Thm.prop_of thm) [];
val Ts = map_filter (fn ((v, i), _) => if member (op =) vs v then
@@ -374,13 +374,13 @@
val cs = maps (fn T => map (pair T) S) Ts;
val constraints' = map Logic.mk_of_class cs;
fun typ_map T = Type.strip_sorts
- (map_atyps (fn U => if member (op =) atyps U then atyp_map U else U) T);
+ (map_atyps (fn U => if member (op =) atyps U then (#atyp_map ucontext) U else U) T);
fun mk_hyp (T, c) = Hyp (Logic.mk_of_class (typ_map T, c));
val xs' = map (map_types typ_map) xs
in
prf |>
Same.commit (Proofterm.map_proof_same (map_types typ_map) typ_map mk_hyp) |>
- fold_rev Proofterm.implies_intr_proof' (map snd constraints) |>
+ fold_rev Proofterm.implies_intr_proof' (map snd (#constraints ucontext)) |>
fold_rev Proofterm.forall_intr_proof' xs' |>
fold_rev Proofterm.implies_intr_proof' constraints'
end;