Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML

--- a/src/Pure/goals.ML	Fri Jan 31 20:12:44 2003 +0100
+++ b/src/Pure/goals.ML	Mon Feb 03 11:04:16 2003 +0100
@@ -108,7 +108,6 @@
   val print_locales: theory -> unit
   val get_thm: theory -> xstring -> thm
   val get_thms: theory -> xstring -> thm list
-  val find_intros_goal : theory -> thm -> int -> (string * thm) list
   val add_locale: bstring -> (bstring option) -> (string * string * mixfix) list ->
     (string * string) list -> (string * string) list -> theory -> theory
   val add_locale_i: bstring -> (bstring option) -> (string * typ * mixfix) list ->
@@ -901,10 +900,7 @@
 fun uresult () = !curr_mkresult (false, topthm());
 
 (*Get subgoal i from goal stack*)
-fun get_goal st i = List.nth (prems_of st, i-1)
-                handle Subscript => error"getgoal: Goal number out of range";
-
-fun getgoal i = get_goal (topthm()) i;
+fun getgoal i = Logic.get_goal (prop_of (topthm())) i;
 
 (*Return subgoal i's hypotheses as meta-level assumptions.
   For debugging uses of METAHYPS*)
@@ -1156,35 +1152,17 @@
     PureThy.thms_containing_consts thy consts
   end;
 
-(*assume that parameters have unique names; reverse them for substitution*)
-fun goal_params st i =
-  let val gi = get_goal st i
-      val rfrees = rev(map Free (Logic.strip_params gi))
-  in (gi,rfrees) end;
-
-fun concl_of_goal st i =
-  let val (gi,rfrees) = goal_params st i
-      val B = Logic.strip_assums_concl gi
-  in subst_bounds(rfrees,B) end;
-
-fun prems_of_goal st i =
-  let val (gi,rfrees) = goal_params st i
-      val As = Logic.strip_assums_hyp gi
-  in map (fn A => subst_bounds(rfrees,A)) As end;
-
-fun find_intros_goal thy st i = PureThy.find_intros thy (concl_of_goal st i);
-
-fun findI i = find_intros_goal (theory_of_goal()) (topthm()) i;
+fun findI i = PureThy.find_intros_goal (theory_of_goal()) (topthm()) i;
 
 fun findEs i =
   let fun eq_nth((n1,th1),(n2,th2)) = n1=n2 andalso eq_thm(th1,th2);
-      val prems = prems_of_goal (topthm()) i
+      val prems = Logic.prems_of_goal (prop_of (topthm())) i
       val thy = theory_of_goal();
       val thmss = map (PureThy.find_elims thy) prems
   in foldl (gen_union eq_nth) ([],thmss) end;
 
 fun findE i j =
-  let val prems = prems_of_goal (topthm()) i
+  let val prems = Logic.prems_of_goal (prop_of (topthm())) i
       val thy = theory_of_goal();
   in PureThy.find_elims thy (nth_elem(j-1, prems)) end;
 

--- a/src/Pure/logic.ML	Fri Jan 31 20:12:44 2003 +0100
+++ b/src/Pure/logic.ML	Mon Feb 03 11:04:16 2003 +0100
@@ -49,6 +49,9 @@
   val assum_pairs       : term -> (term*term)list
   val varify            : term -> term
   val unvarify          : term -> term
+  val get_goal          : term -> int -> term
+  val prems_of_goal     : term -> int -> term list
+  val concl_of_goal     : term -> int -> term
 end;
 
 structure Logic : LOGIC =
@@ -333,4 +336,25 @@
   | unvarify (f$t) = unvarify f $ unvarify t
   | unvarify t = t;
 
+
+(*Get subgoal i*)
+fun get_goal st i = List.nth (strip_imp_prems st, i-1)
+  handle Subscript => error "get_goal: Goal number out of range";
+
+(*reverses parameters for substitution*)
+fun goal_params st i =
+  let val gi = get_goal st i
+      val rfrees = rev (map Free (rename_wrt_term gi (strip_params gi)))
+  in (gi, rfrees) end;
+
+fun concl_of_goal st i =
+  let val (gi, rfrees) = goal_params st i
+      val B = strip_assums_concl gi
+  in subst_bounds (rfrees, B) end;
+
+fun prems_of_goal st i =
+  let val (gi, rfrees) = goal_params st i
+      val As = strip_assums_hyp gi
+  in map (fn A => subst_bounds (rfrees, A)) As end;
+
 end;