# HG changeset patch
# User wenzelm
# Date 1331413365 -3600
# Node ID 152e8ca3264e066beffe49ef562525c8a6209ea9
# Parent  fe8d6532e1c152ef644b345049cc8feeed3ba9b9
eliminated dead code;

diff -r fe8d6532e1c1 -r 152e8ca3264e src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Sat Mar 10 21:25:59 2012 +0100
+++ b/src/Pure/more_thm.ML	Sat Mar 10 22:02:45 2012 +0100
@@ -37,7 +37,6 @@
   val thm_cache: (thm -> 'a) -> thm -> 'a
   val is_reflexive: thm -> bool
   val eq_thm: thm * thm -> bool
-  val eq_thms: thm list * thm list -> bool
   val eq_thm_thy: thm * thm -> bool
   val eq_thm_prop: thm * thm -> bool
   val equiv_thm: thm * thm -> bool
@@ -188,8 +187,6 @@
   Context.joinable (pairself Thm.theory_of_thm ths) andalso
   is_equal (thm_ord ths);
 
-val eq_thms = eq_list eq_thm;
-
 val eq_thm_thy = Theory.eq_thy o pairself Thm.theory_of_thm;
 val eq_thm_prop = op aconv o pairself Thm.full_prop_of;