src/Pure/Thy/thy_output.ML
changeset 39125 f45d332a90e3
parent 38980 af73cf0dc31f
child 39127 e7ecbe86d22e
     1.1 --- a/src/Pure/Thy/thy_output.ML	Fri Sep 03 20:39:38 2010 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Sep 03 21:13:53 2010 +0200
     1.3 @@ -459,7 +459,7 @@
     1.4  val _ = add_option "margin" (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer);
     1.5  val _ = add_option "indent" (Config.put indent o integer);
     1.6  val _ = add_option "source" (Config.put source o boolean);
     1.7 -val _ = add_option "goals_limit" (add_wrapper o setmp_CRITICAL goals_limit o integer);
     1.8 +val _ = add_option "goals_limit" (Config.put Goal_Display.goals_limit o integer);
     1.9  
    1.10  
    1.11  (* basic pretty printing *)
    1.12 @@ -582,7 +582,7 @@
    1.13    | _ => error "No proof state");
    1.14  
    1.15  fun goal_state name main_goal = antiquotation name (Scan.succeed ())
    1.16 -  (fn {state, context, ...} => fn () => output context
    1.17 +  (fn {state, context = ctxt, ...} => fn () => output ctxt
    1.18      [Pretty.chunks (Proof.pretty_goals main_goal (proof_state state))]);
    1.19  
    1.20  in