src/Pure/Isar/proof.ML
changeset 32145 220c9e439d39
parent 32091 30e2ffbba718
child 32167 d32817dda0e6
     1.1 --- a/src/Pure/Isar/proof.ML	Thu Jul 23 16:43:31 2009 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Thu Jul 23 16:52:16 2009 +0200
     1.3 @@ -318,8 +318,6 @@
     1.4  val show_main_goal = ref false;
     1.5  val verbose = ProofContext.verbose;
     1.6  
     1.7 -val pretty_goals_local = Display_Goal.pretty_goals_aux o Syntax.pp;
     1.8 -
     1.9  fun pretty_facts _ _ NONE = []
    1.10    | pretty_facts s ctxt (SOME ths) =
    1.11        [Pretty.big_list (s ^ "this:") (map (Display.pretty_thm ctxt) ths), Pretty.str ""];
    1.12 @@ -346,7 +344,7 @@
    1.13              (if mode <> Backward orelse null using then NONE else SOME using) @
    1.14            [Pretty.str ("goal" ^
    1.15              description [levels_up (i div 2), subgoals (Thm.nprems_of goal)] ^ ":")] @
    1.16 -          pretty_goals_local ctxt Markup.subgoal
    1.17 +          Display_Goal.pretty_goals ctxt Markup.subgoal
    1.18              (true, ! show_main_goal) (! Display.goals_limit) goal @
    1.19            (map (fn msg => Position.setmp_thread_data pos msg ()) (rev messages))
    1.20        | prt_goal NONE = [];
    1.21 @@ -368,7 +366,7 @@
    1.22  
    1.23  fun pretty_goals main state =
    1.24    let val (ctxt, (_, goal)) = get_goal state
    1.25 -  in pretty_goals_local ctxt Markup.none (false, main) (! Display.goals_limit) goal end;
    1.26 +  in Display_Goal.pretty_goals ctxt Markup.none (false, main) (! Display.goals_limit) goal end;
    1.27  
    1.28  
    1.29  
    1.30 @@ -474,7 +472,8 @@
    1.31  
    1.32      val ngoals = Thm.nprems_of goal;
    1.33      val _ = ngoals = 0 orelse error (Pretty.string_of (Pretty.chunks
    1.34 -      (pretty_goals_local ctxt Markup.none (true, ! show_main_goal) (! Display.goals_limit) goal @
    1.35 +      (Display_Goal.pretty_goals ctxt Markup.none
    1.36 +          (true, ! show_main_goal) (! Display.goals_limit) goal @
    1.37          [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")])));
    1.38  
    1.39      val extra_hyps = Assumption.extra_hyps ctxt goal;