# HG changeset patch
# User kleing
# Date 1117009089 -7200
# Node ID e0136cdef722e18702e26187a6819a56eeea904a
# Parent  4a83dd540b8810908b17caadd03101def416b12e
removed obsolete findI, findE, findEs
(and the functions they depended on in Isar/find_theorems)

diff -r 4a83dd540b88 -r e0136cdef722 src/Pure/Isar/find_theorems.ML
--- a/src/Pure/Isar/find_theorems.ML	Wed May 25 09:44:34 2005 +0200
+++ b/src/Pure/Isar/find_theorems.ML	Wed May 25 10:18:09 2005 +0200
@@ -10,9 +10,6 @@
 signature FIND_THEOREMS =
 sig
   val find_thms: Proof.context -> FactIndex.spec -> (thmref * thm) list
-  val find_intros: Proof.context -> term -> (thmref * thm) list
-  val find_intros_goal: Proof.context -> thm -> int -> (thmref * thm) list
-  val find_elims: Proof.context -> term -> (thmref * thm) list
   datatype 'term criterion =
     Name of string | Intro | Elim | Dest | Rewrite of 'term | Pattern of 'term
   val print_theorems: Proof.context -> term option -> int option ->
@@ -82,22 +79,6 @@
 end;
 
 
-(* intro/elim rules *)
-
-(*match statement against conclusion of some rule*)
-val find_intros =
-  find_matching_thms (single, Logic.strip_imp_concl);
-
-(*match conclusion of subgoal i against conclusion of some rule*)
-fun find_intros_goal ctxt st i =
-  find_intros ctxt (Logic.concl_of_goal (Thm.prop_of st) i);
-
-(*match statement against major premise of some rule*)
-val find_elims = find_matching_thms
-  (fn thm => if Thm.no_prems thm then [] else [thm],
-   hd o Logic.strip_imp_prems);
-
-
 
 (** search criteria **)
 
diff -r 4a83dd540b88 -r e0136cdef722 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Wed May 25 09:44:34 2005 +0200
+++ b/src/Pure/goals.ML	Wed May 25 10:18:09 2005 +0200
@@ -96,9 +96,6 @@
     -> (thm list -> tactic list) -> unit
   val no_qed: unit -> unit
   val thms_containing   : xstring list -> (string * thm) list
-  val findI             : int -> (thmref * thm) list
-  val findEs            : int -> (thmref * thm) list
-  val findE             : int -> int -> (thmref * thm) list
 end;
 
 signature GOALS =
@@ -1147,18 +1144,6 @@
     PureThy.thms_containing_consts thy consts
   end;
 
-fun findI i = FindTheorems.find_intros_goal (context_of_goal()) (topthm()) i;
-
-fun findEs i =
-  let fun eq_nth((n1,th1),(n2,th2)) = n1=n2 andalso eq_thm(th1,th2);
-      val prems = Logic.prems_of_goal (prop_of (topthm())) i
-      val thmss = map (FindTheorems.find_elims (context_of_goal ())) prems
-  in Library.foldl (gen_union eq_nth) ([],thmss) end;
-
-fun findE i j =
-  let val prems = Logic.prems_of_goal (prop_of (topthm())) i
-  in FindTheorems.find_elims (context_of_goal ()) (List.nth(prems, j-1)) end;
-
 end;
 
 structure BasicGoals: BASIC_GOALS = Goals;