diff -r 947152add153 -r 707639e9497d src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Jul 23 14:06:11 2007 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Jul 23 14:06:12 2007 +0200
@@ -455,9 +455,9 @@
 
 val prepare_dummies =
   let val next = ref 1 in
-    fn t =>
+    fn t => CRITICAL (fn () =>
       let val (i, u) = Term.replace_dummy_patterns (! next, t)
-      in next := i; u end
+      in next := i; u end)
   end;
 
 fun reject_dummies t = Term.no_dummy_patterns t