1.1 --- a/src/Pure/more_thm.ML	Sat Mar 10 21:25:59 2012 +0100
     1.2 +++ b/src/Pure/more_thm.ML	Sat Mar 10 22:02:45 2012 +0100
     1.3 @@ -37,7 +37,6 @@
     1.4    val thm_cache: (thm -> 'a) -> thm -> 'a
     1.5    val is_reflexive: thm -> bool
     1.6    val eq_thm: thm * thm -> bool
     1.7 -  val eq_thms: thm list * thm list -> bool
     1.8    val eq_thm_thy: thm * thm -> bool
     1.9    val eq_thm_prop: thm * thm -> bool
    1.10    val equiv_thm: thm * thm -> bool
    1.11 @@ -188,8 +187,6 @@
    1.12    Context.joinable (pairself Thm.theory_of_thm ths) andalso
    1.13    is_equal (thm_ord ths);
    1.14  
    1.15 -val eq_thms = eq_list eq_thm;
    1.16 -
    1.17  val eq_thm_thy = Theory.eq_thy o pairself Thm.theory_of_thm;
    1.18  val eq_thm_prop = op aconv o pairself Thm.full_prop_of;
    1.19