src/Pure/Isar/proof_context.ML
changeset 39508 dfacdb01e1ec
parent 39507 839873937ddd
child 39557 fe5722fce758
--- 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