simplified some internal flags using Config.T instead of full-blown Proof_Data;

--- a/src/Pure/Isar/proof_context.ML	Fri Sep 17 20:18:27 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri Sep 17 20:42:26 2010 +0200
@@ -585,17 +585,17 @@
 
 local
 
-structure Allow_Dummies = Proof_Data(type T = bool fun init _ = false);
+val dummies = Config.bool (Config.declare "ProofContext.dummies" (K (Config.Bool false)));
 
 fun check_dummies ctxt t =
-  if Allow_Dummies.get ctxt then t
+  if Config.get ctxt dummies then t
   else Term.no_dummy_patterns t handle TERM _ => error "Illegal dummy pattern(s) in term";
 
 fun prepare_dummies ts = #1 (fold_map Term.replace_dummy_patterns ts 1);
 
 in
 
-val allow_dummies = Allow_Dummies.put true;
+val allow_dummies = Config.put dummies true;
 
 fun prepare_patterns ctxt =
   let val Mode {pattern, ...} = get_mode ctxt in

--- a/src/Pure/ROOT.ML	Fri Sep 17 20:18:27 2010 +0200
+++ b/src/Pure/ROOT.ML	Fri Sep 17 20:42:26 2010 +0200
@@ -96,13 +96,13 @@
 use "old_term.ML";
 use "General/pretty.ML";
 use "context.ML";
+use "config.ML";
 use "context_position.ML";
 use "sorts.ML";
 use "type.ML";
 use "logic.ML";
 use "Syntax/lexicon.ML";
 use "Syntax/simple_syntax.ML";
-use "config.ML";
 
 
 (* inner syntax *)

--- a/src/Pure/Syntax/syntax.ML	Fri Sep 17 20:18:27 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML	Fri Sep 17 20:42:26 2010 +0200
@@ -361,9 +361,9 @@
 
 (* global pretty printing *)
 
-structure PrettyGlobal = Proof_Data(type T = bool fun init _ = false);
-val is_pretty_global = PrettyGlobal.get;
-val set_pretty_global = PrettyGlobal.put;
+val pretty_global = Config.bool (Config.declare "Syntax.pretty_global" (K (Config.Bool false)));
+fun is_pretty_global ctxt = Config.get ctxt pretty_global;
+val set_pretty_global = Config.put pretty_global;
 val init_pretty_global = set_pretty_global true o ProofContext.init_global;
 
 val pretty_term_global = pretty_term o init_pretty_global;

--- a/src/Pure/context_position.ML	Fri Sep 17 20:18:27 2010 +0200
+++ b/src/Pure/context_position.ML	Fri Sep 17 20:42:26 2010 +0200
@@ -18,14 +18,9 @@
 structure Context_Position: CONTEXT_POSITION =
 struct
 
-structure Data = Proof_Data
-(
-  type T = bool;
-  fun init _ = true;
-);
-
-val is_visible = Data.get;
-val set_visible = Data.put;
+val visible = Config.bool (Config.declare "Context_Position.visible" (K (Config.Bool true)));
+fun is_visible ctxt = Config.get ctxt visible;
+val set_visible = Config.put visible;
 val restore_visible = set_visible o is_visible;
 
 fun if_visible ctxt f x = if is_visible ctxt then f x else ();