# HG changeset patch
# User wenzelm
# Date 964475234 -7200
# Node ID 96973ec6fda45d5a08086d673650efcb92abc9eb
# Parent  c4f7c959eaee692ea8dc63f56dd447cd0cd62fd9
Drule.merge_rules;

diff -r c4f7c959eaee -r 96973ec6fda4 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sun Jul 23 12:10:41 2000 +0200
+++ b/src/Pure/Isar/method.ML	Mon Jul 24 23:47:14 2000 +0200
@@ -120,8 +120,6 @@
 fun print_rules (intro, elim) =
   (prt_rules "introduction" intro; prt_rules "elimination" elim);
 
-fun merge_rules (ths1, ths2) = Library.generic_merge Thm.eq_thm I I ths1 ths2;
-
 
 (* theory data kind 'Isar/rules' *)
 
@@ -134,7 +132,7 @@
   val copy = I;
   val prep_ext = I;
   fun merge ((intro1, elim1), (intro2, elim2)) =
-    (merge_rules (intro1, intro2), merge_rules (elim1, elim2));
+    (Drule.merge_rules (intro1, intro2), Drule.merge_rules (elim1, elim2));
   fun print _ = print_rules;
 end;
 
diff -r c4f7c959eaee -r 96973ec6fda4 src/Pure/drule.ML
--- 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;