| changeset 22095 | 07875394618e |
| parent 22089 | d9b614dc883d |
| child 22135 | cd3c167e6f19 |
--- a/src/Pure/Isar/toplevel.ML Fri Jan 19 22:08:01 2007 +0100 +++ b/src/Pure/Isar/toplevel.ML Fri Jan 19 22:08:02 2007 +0100 @@ -267,7 +267,7 @@ local fun with_context f xs = - (case Context.get_context () of NONE => [] + (case ML_Context.get_context () of NONE => [] | SOME context => map (f (Context.proof_of context)) xs); fun raised name [] = "exception " ^ name ^ " raised"