src/Pure/proofterm.ML
changeset 32785 ec5292653aff
parent 32738 15bb09ca0378
child 32810 f3466a5645fa
     1.1 --- a/src/Pure/proofterm.ML	Wed Sep 30 22:20:58 2009 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Wed Sep 30 22:24:57 2009 +0200
     1.3 @@ -959,7 +959,7 @@
     1.4    if ! proofs = 0 then ((name, dummy), Oracle (name, dummy, NONE))
     1.5    else ((name, prop), gen_axm_proof Oracle name prop);
     1.6  
     1.7 -fun shrink_proof thy =
     1.8 +val shrink_proof =
     1.9    let
    1.10      fun shrink ls lev (prf as Abst (a, T, body)) =
    1.11            let val (b, is, ch, body') = shrink ls (lev+1) body
    1.12 @@ -1319,7 +1319,7 @@
    1.13  
    1.14      val proof0 =
    1.15        if ! proofs = 2 then
    1.16 -        #4 (shrink_proof thy [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf)))
    1.17 +        #4 (shrink_proof [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf)))
    1.18        else MinProof;
    1.19      val body0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
    1.20