src/Pure/Isar/proof.ML

 (** pretty_state **)
 
 val show_main_goal = ref false;
 val verbose = ProofContext.verbose;
 
-val pretty_goals_local = Display_Goal.pretty_goals_aux o Syntax.pp;
-
 fun pretty_facts _ _ NONE = []
   | pretty_facts s ctxt (SOME ths) =
       [Pretty.big_list (s ^ "this:") (map (Display.pretty_thm ctxt) ths), Pretty.str ""];
 
 fun pretty_state nr state =

       {statement = ((_, pos), _, _), messages, using, goal, before_qed = _, after_qed = _}))) =
           pretty_facts "using " ctxt
             (if mode <> Backward orelse null using then NONE else SOME using) @
           [Pretty.str ("goal" ^
             description [levels_up (i div 2), subgoals (Thm.nprems_of goal)] ^ ":")] @
-          pretty_goals_local ctxt Markup.subgoal
+          Display_Goal.pretty_goals ctxt Markup.subgoal
             (true, ! show_main_goal) (! Display.goals_limit) goal @
           (map (fn msg => Position.setmp_thread_data pos msg ()) (rev messages))
       | prt_goal NONE = [];
 
     val prt_ctxt =

      else prt_goal (try find_goal state))
   end;
 
 fun pretty_goals main state =
   let val (ctxt, (_, goal)) = get_goal state
-  in pretty_goals_local ctxt Markup.none (false, main) (! Display.goals_limit) goal end;
+  in Display_Goal.pretty_goals ctxt Markup.none (false, main) (! Display.goals_limit) goal end;
 
 
 
 (** proof steps **)
 

     val string_of_term = Syntax.string_of_term ctxt;
     val string_of_thm = Display.string_of_thm ctxt;
 
     val ngoals = Thm.nprems_of goal;
     val _ = ngoals = 0 orelse error (Pretty.string_of (Pretty.chunks
-      (pretty_goals_local ctxt Markup.none (true, ! show_main_goal) (! Display.goals_limit) goal @
+      (Display_Goal.pretty_goals ctxt Markup.none
+          (true, ! show_main_goal) (! Display.goals_limit) goal @
         [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")])));
 
     val extra_hyps = Assumption.extra_hyps ctxt goal;
     val _ = null extra_hyps orelse
       error ("Additional hypotheses:\n" ^ cat_lines (map string_of_term extra_hyps));