changeset 25269 | f9090ae5cec9 |
parent 25192 | b568f8c5d5ca |
child 25290 | 250c7a0205ca |
--- a/src/Pure/Isar/isar_syn.ML Fri Nov 02 18:52:59 2007 +0100 +++ b/src/Pure/Isar/isar_syn.ML Fri Nov 02 18:53:00 2007 +0100 @@ -387,7 +387,7 @@ val _ = OuterSyntax.command "context" "enter local theory context" K.thy_decl (P.name --| P.begin >> (fn name => - Toplevel.print o Toplevel.begin_local_theory true (TheoryTarget.init_cmd (SOME name)))); + Toplevel.print o Toplevel.begin_local_theory true (TheoryTarget.init_cmd name))); (* locales *)