changeset 49865 | eeaf1ec7eac2 |
parent 46218 | ecf6375e2abb |
child 56243 | 2e10a36b8d46 |
--- 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 =