--- a/src/Pure/logic.ML Fri Jul 11 14:59:50 2003 +0200
+++ b/src/Pure/logic.ML Fri Jul 11 15:00:10 2003 +0200
@@ -50,6 +50,7 @@
val varify : term -> term
val unvarify : term -> term
val get_goal : term -> int -> term
+ val goal_params : term -> int -> term * term list
val prems_of_goal : term -> int -> term list
val concl_of_goal : term -> int -> term
end;
@@ -339,7 +340,7 @@
(*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";
+ handle Subscript => error "Goal number out of range";
(*reverses parameters for substitution*)
fun goal_params st i =