src/Pure/goal_display.ML

--- a/src/Pure/goal_display.ML	Mon Sep 06 19:23:54 2010 +0200
+++ b/src/Pure/goal_display.ML	Mon Sep 06 21:33:19 2010 +0200
@@ -8,14 +8,14 @@
 signature GOAL_DISPLAY =
 sig
   val goals_limit_default: int Unsynchronized.ref
-  val goals_limit_value: Config.value Config.T
+  val goals_limit_raw: Config.raw
   val goals_limit: int Config.T
   val goals_total: bool Config.T
   val show_main_goal_default: bool Unsynchronized.ref
-  val show_main_goal_value: Config.value Config.T
+  val show_main_goal_raw: Config.raw
   val show_main_goal: bool Config.T
   val show_consts_default: bool Unsynchronized.ref
-  val show_consts_value: Config.value Config.T
+  val show_consts_raw: Config.raw
   val show_consts: bool Config.T
   val pretty_flexpair: Proof.context -> term * term -> Pretty.T
   val pretty_goals: Proof.context -> thm -> Pretty.T list
@@ -26,19 +26,19 @@
 struct
 
 val goals_limit_default = Unsynchronized.ref 10;
-val goals_limit_value = Config.declare "goals_limit" (fn _ => Config.Int (! goals_limit_default));
-val goals_limit = Config.int goals_limit_value;
+val goals_limit_raw = Config.declare "goals_limit" (fn _ => Config.Int (! goals_limit_default));
+val goals_limit = Config.int goals_limit_raw;
 
 val goals_total = Config.bool (Config.declare "goals_total" (fn _ => Config.Bool true));
 
 val show_main_goal_default = Unsynchronized.ref false;
-val show_main_goal_value =
+val show_main_goal_raw =
   Config.declare "show_main_goal" (fn _ => Config.Bool (! show_main_goal_default));
-val show_main_goal = Config.bool show_main_goal_value;
+val show_main_goal = Config.bool show_main_goal_raw;
 
 val show_consts_default = Unsynchronized.ref false;
-val show_consts_value = Config.declare "show_consts" (fn _ => Config.Bool (! show_consts_default));
-val show_consts = Config.bool show_consts_value;
+val show_consts_raw = Config.declare "show_consts" (fn _ => Config.Bool (! show_consts_default));
+val show_consts = Config.bool show_consts_raw;
 
 fun pretty_flexpair ctxt (t, u) = Pretty.block
   [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];