# HG changeset patch
# User berghofe
# Date 1057928410 -7200
# Node ID 215585ac94e242ca20b8c29523556d543d8e362e
# Parent  bbf708a7e27f8da10e6a1ca20cca98b938b7abe2
Exported function goal_params.

diff -r bbf708a7e27f -r 215585ac94e2 src/Pure/logic.ML
--- 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 =