--- 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;