author | wenzelm |
Mon, 05 Nov 2007 20:50:43 +0100 | |
changeset 25290 | 250c7a0205ca |
parent 25289 | 3d332d8a827c |
child 25291 | 870455627720 |
--- 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 *)