changeset 25290 | 250c7a0205ca |
parent 25269 | f9090ae5cec9 |
child 25462 | dad0291cb76a |
--- a/src/Pure/Isar/isar_syn.ML Mon Nov 05 20:50:42 2007 +0100 +++ b/src/Pure/Isar/isar_syn.ML Mon Nov 05 20:50:43 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 name))); + Toplevel.print o Toplevel.begin_local_theory true (TheoryTarget.context name))); (* locales *)