# HG changeset patch
# User wenzelm
# Date 1187635443 -7200
# Node ID c4dcc740822614fc874a1e673fc81ed61d493dce
# Parent  a9fe7ed25fa4c14f6dafe35cbc1c5b708ec7f10d
prepare_dummies: NAMED_CRITICAL;

diff -r a9fe7ed25fa4 -r c4dcc7408226 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Aug 20 20:44:02 2007 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Aug 20 20:44:03 2007 +0200
@@ -498,7 +498,7 @@
 
 val prepare_dummies =
   let val next = ref 1 in
-    fn t => CRITICAL (fn () =>
+    fn t => NAMED_CRITICAL "prepare_dummies" (fn () =>
       let val (i, u) = Term.replace_dummy_patterns (! next, t)
       in next := i; u end)
   end;