src/Pure/display_goal.ML

   val show_consts: bool ref
   val pretty_flexpair: Proof.context -> term * term -> Pretty.T
   val pretty_goals: Proof.context -> {total: bool, main: bool, maxgoals: int} ->
     thm -> Pretty.T list
   val pretty_goals_without_context: int -> thm -> Pretty.T list
-  val print_goals_without_context: int -> thm -> unit
 end;
 
 structure Display_Goal: DISPLAY_GOAL =
 struct
 

 
 fun pretty_goals_without_context n th =
   pretty_goals (Syntax.init_pretty_global (Thm.theory_of_thm th))
     {total = true, main = true, maxgoals = n} th;
 
-val print_goals_without_context =
-  (Pretty.writeln o Pretty.chunks) oo pretty_goals_without_context;
-
 end;
 
 end;