changeset 21506 | b2a673894ce5 |
parent 21401 | faddc6504177 |
child 21858 | 05f57309170c |
--- a/src/Pure/Isar/outer_syntax.ML Thu Nov 23 22:38:29 2006 +0100 +++ b/src/Pure/Isar/outer_syntax.ML Thu Nov 23 22:38:30 2006 +0100 @@ -328,7 +328,7 @@ val exn = Toplevel.exn; fun context () = - Context.proof_of (Toplevel.context_of (state ())) + Toplevel.context_of (state ()) handle Toplevel.UNDEF => error "Unknown context"; fun goal () =