diff -r 34437e7245cc -r eeaf1ec7eac2 src/Pure/logic.ML --- a/src/Pure/logic.ML Tue Oct 16 16:50:03 2012 +0200 +++ b/src/Pure/logic.ML Tue Oct 16 17:47:23 2012 +0200 @@ -557,8 +557,10 @@ (* goal states *) -fun get_goal st i = nth_prem (i, st) - handle TERM _ => error "Goal number out of range"; +fun get_goal st i = + nth_prem (i, st) handle TERM _ => + error ("Subgoal number " ^ string_of_int i ^ " out of range (a total of " ^ + string_of_int (count_prems st) ^ " subgoals)"); (*reverses parameters for substitution*) fun goal_params st i =