| changeset 47060 | e2741ec9ae36 |
| parent 47005 | 421760a1efe7 |
| child 47065 | cce369d41d50 |
--- a/src/Pure/Isar/proof.ML Tue Mar 20 21:37:31 2012 +0100 +++ b/src/Pure/Isar/proof.ML Wed Mar 21 11:00:34 2012 +0100 @@ -183,7 +183,7 @@ fun open_block (State st) = State (Stack.push st); fun close_block (State st) = State (Stack.pop st) - handle Empty => error "Unbalanced block parentheses"; + handle List.Empty => error "Unbalanced block parentheses"; fun level (State st) = Stack.level st;