author | wenzelm |
Mon, 20 Aug 2007 20:44:03 +0200 | |
changeset 24363 | c4dcc7408226 |
parent 24362 | a9fe7ed25fa4 |
child 24364 | 31e359126ab6 |
--- 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;