# 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 ****)