# HG changeset patch
# User wenzelm
# Date 1231079320 -3600
# Node ID 5904873d8f11937aff5086062a703c1114569b30
# Parent  fc4a04a2970ad4f4995696b0eb47acb23915b406
tuned protect, conclude: Drule.comp_no_flatten;

diff -r fc4a04a2970a -r 5904873d8f11 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Sun Jan 04 15:28:09 2009 +0100
+++ b/src/Pure/goal.ML	Sun Jan 04 15:28:40 2009 +0100
@@ -1,6 +1,5 @@
 (*  Title:      Pure/goal.ML
-    ID:         $Id$
-    Author:     Makarius and Lawrence C Paulson
+    Author:     Makarius
 
 Goals in tactical theorem proving.
 *)
@@ -58,18 +57,14 @@
   --- (protect)
   #C
 *)
-fun protect th = th COMP_INCR Drule.protectI;
+fun protect th = Drule.comp_no_flatten (th, 0) 1 Drule.protectI;
 
 (*
   A ==> ... ==> #C
   ---------------- (conclude)
   A ==> ... ==> C
 *)
-fun conclude th =
-  (case SINGLE (Thm.compose_no_flatten false (th, Thm.nprems_of th) 1)
-      (Drule.incr_indexes th Drule.protectD) of
-    SOME th' => th'
-  | NONE => raise THM ("Failed to conclude goal", 0, [th]));
+fun conclude th = Drule.comp_no_flatten (th, Thm.nprems_of th) 1 Drule.protectD;
 
 (*
   #C