src/Pure/Isar/isar_syn.ML
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