src/Pure/goal_display.ML

   val show_consts_raw: Config.raw
   val show_consts: bool Config.T
   val pretty_flexpair: Proof.context -> term * term -> Pretty.T
   val pretty_goals: Proof.context -> thm -> Pretty.T list
   val pretty_goals_without_context: thm -> Pretty.T list
-  val pretty_goal: {main: bool, limit: bool} -> Proof.context -> thm -> Pretty.T
+  val pretty_goal: Proof.context -> thm -> Pretty.T
+  val string_of_goal: Proof.context -> thm -> string
 end;
 
 structure Goal_Display: GOAL_DISPLAY =
 struct
 

 fun pretty_goals_without_context th =
   let val ctxt =
     Config.put show_main_goal true (Syntax.init_pretty_global (Thm.theory_of_thm th))
   in pretty_goals ctxt th end;
 
-fun pretty_goal {main, limit} ctxt th =
-  Pretty.chunks (pretty_goals
-    (ctxt
-      |> Config.put show_main_goal main
-      |> not limit ? Config.put goals_limit (Thm.nprems_of th)
-      |> Config.put goals_total false) th);
+fun pretty_goal ctxt th =
+  Pretty.chunks (pretty_goals (Config.put goals_total false ctxt) th);
+
+val string_of_goal = Pretty.string_of oo pretty_goal;
 
 end;
 
 end;