# HG changeset patch
# User wenzelm
# Date 1238256498 -3600
# Node ID 7921fcef927cffc5a94d6e3a0c34e08c8e489136
# Parent  2d2076300185fef1b321b104208690c9563bbf10
tuned;

diff -r 2d2076300185 -r 7921fcef927c src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Mar 28 16:31:16 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sat Mar 28 17:08:18 2009 +0100
@@ -541,17 +541,17 @@
 
 local
 
-structure AllowDummies = ProofDataFun(type T = bool fun init _ = false);
+structure Allow_Dummies = ProofDataFun(type T = bool fun init _ = false);
 
 fun check_dummies ctxt t =
-  if AllowDummies.get ctxt then t
+  if Allow_Dummies.get ctxt 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 = AllowDummies.put true;
+val allow_dummies = Allow_Dummies.put true;
 
 fun prepare_patterns ctxt =
   let val Mode {pattern, ...} = get_mode ctxt in