# HG changeset patch
# User wenzelm
# Date 1231079289 -3600
# Node ID fc4a04a2970ad4f4995696b0eb47acb23915b406
# Parent  43ac99cdeb5b4def178afec6aa45265334bfebd1
added comp_no_flatten;

diff -r 43ac99cdeb5b -r fc4a04a2970a src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sun Jan 04 00:01:16 2009 +0100
+++ b/src/Pure/drule.ML	Sun Jan 04 15:28:09 2009 +0100
@@ -110,6 +110,7 @@
   val sort_triv: theory -> typ * sort -> thm list
   val unconstrainTs: thm -> thm
   val with_subgoal: int -> (thm -> thm) -> thm -> thm
+  val comp_no_flatten: thm * int -> int -> thm -> thm
   val rename_bvars: (string * string) list -> thm -> thm
   val rename_bvars': string option list -> thm -> thm
   val incr_type_indexes: int -> thm -> thm
@@ -818,6 +819,14 @@
 fun th1 INCR_COMP th2 = incr_indexes th2 th1 COMP th2;
 fun th1 COMP_INCR th2 = th1 COMP incr_indexes th1 th2;
 
+fun comp_no_flatten (th, n) i rule =
+  (case distinct Thm.eq_thm (Seq.list_of
+      (Thm.compose_no_flatten false (th, n) i (incr_indexes th rule))) of
+    [th'] => th'
+  | [] => raise THM ("comp_no_flatten", i, [th, rule])
+  | _ => raise THM ("comp_no_flatten: unique result expected", i, [th, rule]));
+
+
 
 (*** Instantiate theorem th, reading instantiations in theory thy ****)