equal
deleted
inserted
replaced
712 |
712 |
713 fun prep_thm (thm, vs) = |
713 fun prep_thm (thm, vs) = |
714 let |
714 let |
715 val thy = Thm.theory_of_thm thm; |
715 val thy = Thm.theory_of_thm thm; |
716 val prop = Thm.prop_of thm; |
716 val prop = Thm.prop_of thm; |
717 val prf = proof_of (Thm.proof_of thm); |
717 val prf = Thm.proof_of thm; |
718 val name = Thm.get_name thm; |
718 val name = Thm.get_name thm; |
719 val _ = name <> "" orelse error "extraction: unnamed theorem"; |
719 val _ = name <> "" orelse error "extraction: unnamed theorem"; |
720 val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^ |
720 val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^ |
721 quote name ^ " has no computational content") |
721 quote name ^ " has no computational content") |
722 in (Reconstruct.reconstruct_proof thy prop prf, vs) end; |
722 in (Reconstruct.reconstruct_proof thy prop prf, vs) end; |