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