src/Pure/proofterm.ML
changeset 11999 43b4385445bf
parent 11715 592923615f77
child 12041 27214c16ebe4
equal deleted inserted replaced
11998:b14e7686ce84 11999:43b4385445bf
  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