skip_proofs: do not skip proofs of schematic goals (warning);
authorwenzelm
Tue Jul 04 18:39:59 2006 +0200 (2006-07-04)
changeset 19996a4332e71c1de
parent 19995 7f841a2b431c
child 19997 fe69952f09f6
skip_proofs: do not skip proofs of schematic goals (warning);
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Tue Jul 04 18:39:58 2006 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Jul 04 18:39:59 2006 +0200
     1.3 @@ -464,9 +464,17 @@
     1.4  
     1.5  fun theory_to_proof f = app_current (fn int =>
     1.6    (fn Theory (thy, _) =>
     1.7 -    if ! skip_proofs then
     1.8 -      SkipProof ((History.init (undo_limit int) 0, #2 (Proof.global_skip_proof int (f thy))), thy)
     1.9 -    else Proof (ProofHistory.init (undo_limit int) (f thy), thy)
    1.10 +    let
    1.11 +      val prf = f thy;
    1.12 +      val schematic = Proof.schematic_goal prf;
    1.13 +    in
    1.14 +      if ! skip_proofs andalso schematic then
    1.15 +        warning "Cannot skip proof of schematic goal statement"
    1.16 +      else ();
    1.17 +      if ! skip_proofs andalso not schematic then
    1.18 +        SkipProof ((History.init (undo_limit int) 0, #2 (Proof.global_skip_proof int prf)), thy)
    1.19 +      else Proof (ProofHistory.init (undo_limit int) prf, thy)
    1.20 +    end
    1.21    | _ => raise UNDEF));
    1.22  
    1.23  fun proofs' f = map_current (fn int =>