src/Pure/goal.ML
changeset 29345 5904873d8f11
parent 29343 43ac99cdeb5b
child 29435 a5f84ac14609
     1.1 --- a/src/Pure/goal.ML	Sun Jan 04 15:28:09 2009 +0100
     1.2 +++ b/src/Pure/goal.ML	Sun Jan 04 15:28:40 2009 +0100
     1.3 @@ -1,6 +1,5 @@
     1.4  (*  Title:      Pure/goal.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Makarius and Lawrence C Paulson
     1.7 +    Author:     Makarius
     1.8  
     1.9  Goals in tactical theorem proving.
    1.10  *)
    1.11 @@ -58,18 +57,14 @@
    1.12    --- (protect)
    1.13    #C
    1.14  *)
    1.15 -fun protect th = th COMP_INCR Drule.protectI;
    1.16 +fun protect th = Drule.comp_no_flatten (th, 0) 1 Drule.protectI;
    1.17  
    1.18  (*
    1.19    A ==> ... ==> #C
    1.20    ---------------- (conclude)
    1.21    A ==> ... ==> C
    1.22  *)
    1.23 -fun conclude th =
    1.24 -  (case SINGLE (Thm.compose_no_flatten false (th, Thm.nprems_of th) 1)
    1.25 -      (Drule.incr_indexes th Drule.protectD) of
    1.26 -    SOME th' => th'
    1.27 -  | NONE => raise THM ("Failed to conclude goal", 0, [th]));
    1.28 +fun conclude th = Drule.comp_no_flatten (th, Thm.nprems_of th) 1 Drule.protectD;
    1.29  
    1.30  (*
    1.31    #C