changeset 70436 | 251f1fb44ccd |
parent 70435 | 52fbcf7a61f8 |
child 70443 | a21a96eda033 |
--- a/src/Pure/Proof/reconstruct.ML Mon Jul 29 10:26:12 2019 +0200 +++ b/src/Pure/Proof/reconstruct.ML Mon Jul 29 11:09:37 2019 +0200 @@ -379,7 +379,7 @@ fun clean_proof_of ctxt full thm = let - val {prop, ...} = + val (_, prop) = Logic.unconstrainT (Thm.shyps_of thm) (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm)); in