1029 map Some (sort (make_ord atless) (term_frees prop)); |
1029 map Some (sort (make_ord atless) (term_frees prop)); |
1030 val opt_prf = if ! proofs = 2 then |
1030 val opt_prf = if ! proofs = 2 then |
1031 #4 (shrink [] 0 (rewrite_prf fst (!(ProofData.get_sg sign)) |
1031 #4 (shrink [] 0 (rewrite_prf fst (!(ProofData.get_sg sign)) |
1032 (foldr (uncurry implies_intr_proof) (hyps', prf)))) |
1032 (foldr (uncurry implies_intr_proof) (hyps', prf)))) |
1033 else MinProof (mk_min_proof ([], prf)); |
1033 else MinProof (mk_min_proof ([], prf)); |
1034 val head = (case strip_combt (fst (strip_combP prf)) of |
1034 val head = (case strip_combt (fst (strip_combP opt_prf)) of |
1035 (PThm ((old_name, _), prf', prop', None), args') => |
1035 (PThm ((old_name, _), prf', prop', None), args') => |
1036 if (old_name="" orelse old_name=name) andalso |
1036 if (old_name="" orelse old_name=name) andalso |
1037 prop = prop' andalso args = args' then |
1037 prop = prop' andalso args = args' then |
1038 PThm ((name, tags), prf', prop, None) |
1038 PThm ((name, tags), prf', prop, None) |
1039 else |
1039 else |