1.1 --- a/src/Pure/Isar/proof.ML	Fri Sep 03 11:21:58 2010 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Fri Sep 03 11:27:35 2010 +0200
     1.3 @@ -331,7 +331,7 @@
     1.4  
     1.5  fun pretty_state nr state =
     1.6    let
     1.7 -    val {context, facts, mode, goal = _} = current state;
     1.8 +    val {context = ctxt, facts, mode, goal = _} = current state;
     1.9  
    1.10      fun levels_up 0 = ""
    1.11        | levels_up 1 = "1 level up"
    1.12 @@ -345,7 +345,7 @@
    1.13        (case filter_out (fn s => s = "") strs of [] => ""
    1.14        | strs' => enclose " (" ")" (commas strs'));
    1.15  
    1.16 -    fun prt_goal (SOME (ctxt, (i,
    1.17 +    fun prt_goal (SOME (_, (i,
    1.18        {statement = ((_, pos), _, _), messages, using, goal, before_qed = _, after_qed = _}))) =
    1.19            pretty_facts "using " ctxt
    1.20              (if mode <> Backward orelse null using then NONE else SOME using) @
    1.21 @@ -357,8 +357,8 @@
    1.22        | prt_goal NONE = [];
    1.23  
    1.24      val prt_ctxt =
    1.25 -      if ! verbose orelse mode = Forward then ProofContext.pretty_context context
    1.26 -      else if mode = Backward then ProofContext.pretty_ctxt context
    1.27 +      if ! verbose orelse mode = Forward then ProofContext.pretty_context ctxt
    1.28 +      else if mode = Backward then ProofContext.pretty_ctxt ctxt
    1.29        else [];
    1.30    in
    1.31      [Pretty.str ("proof (" ^ mode_name mode ^ "): step " ^ string_of_int nr ^
    1.32 @@ -366,8 +366,8 @@
    1.33        Pretty.str ""] @
    1.34      (if null prt_ctxt then [] else prt_ctxt @ [Pretty.str ""]) @
    1.35      (if ! verbose orelse mode = Forward then
    1.36 -       pretty_facts "" context facts @ prt_goal (try find_goal state)
    1.37 -     else if mode = Chain then pretty_facts "picking " context facts
    1.38 +       pretty_facts "" ctxt facts @ prt_goal (try find_goal state)
    1.39 +     else if mode = Chain then pretty_facts "picking " ctxt facts
    1.40       else prt_goal (try find_goal state))
    1.41    end;
    1.42