--- a/src/Pure/drule.ML Sun Jul 23 12:10:41 2000 +0200
+++ b/src/Pure/drule.ML Mon Jul 24 23:47:14 2000 +0200
@@ -87,6 +87,7 @@
sig
include BASIC_DRULE
val compose_single : thm * int * thm -> thm
+ val merge_rules : thm list * thm list -> thm list
val triv_goal : thm
val rev_triv_goal : thm
val freeze_all : thm -> thm
@@ -374,6 +375,7 @@
(*Do the two theorems have the same signature?*)
fun eq_thm_sg (th1,th2) = Sign.eq_sg(#sign(rep_thm th1), #sign(rep_thm th2));
+fun merge_rules (ths1, ths2) = Library.generic_merge Thm.eq_thm I I ths1 ths2;
(*Useful "distance" function for BEST_FIRST*)
val size_of_thm = size_of_term o #prop o rep_thm;