src/Pure/goals.ML
changeset 6912 6721243019e7
parent 6390 5d58c100ca3f
child 6960 54d4d1602068
equal deleted inserted replaced
6911:ef0f25d0bc2d 6912:6721243019e7
   316 fun print_current_goals_default n max th =
   316 fun print_current_goals_default n max th =
   317   let val ref (begin_state, end_state, begin_goal) = current_goals_markers;
   317   let val ref (begin_state, end_state, begin_goal) = current_goals_markers;
   318       val ngoals = nprems_of th in
   318       val ngoals = nprems_of th in
   319     writeln (begin_state ^ "Level " ^ string_of_int n ^ 
   319     writeln (begin_state ^ "Level " ^ string_of_int n ^ 
   320 	" (" ^ string_of_int ngoals ^ " subgoal" ^ 
   320 	" (" ^ string_of_int ngoals ^ " subgoal" ^ 
   321 	   (if ngoals > 1 then "s" else "") ^ ")");
   321 	   (if ngoals <> 1 then "s" else "") ^ ")");
   322     Locale.print_goals_marker begin_goal max th;
   322     Locale.print_goals_marker begin_goal max th;
   323     if end_state = "" then () else writeln end_state
   323     if end_state = "" then () else writeln end_state
   324   end;
   324   end;
   325 
   325 
   326 val print_current_goals_fn = ref print_current_goals_default;
   326 val print_current_goals_fn = ref print_current_goals_default;