src/Pure/Isar/proof_context.ML

 
 (* dummy patterns *)
 
 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
   handle TERM _ => error "Illegal dummy pattern(s) in term";