changeset 47870 | 1c3c185bab4e |
parent 47845 | 7ca3608146d8 |
child 47928 | 12423b36fcc4 |
1.1 --- a/src/Pure/Isar/isar_syn.ML Sat Mar 17 17:58:40 2012 +0100 1.2 +++ b/src/Pure/Isar/isar_syn.ML Sat Mar 17 22:46:19 2012 +0100 1.3 @@ -410,7 +410,7 @@ 1.4 1.5 val _ = 1.6 Outer_Syntax.command ("context", Keyword.thy_decl) "enter local theory context" 1.7 - (Parse.position Parse.name --| Parse.begin >> (fn name => 1.8 + (Parse.position Parse.xname --| Parse.begin >> (fn name => 1.9 Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name))); 1.10 1.11