src/Pure/Isar/isar_syn.ML
changeset 25794 11bec58fc289
parent 25625 35e2aa8b8b03
child 25861 494d9301cc75
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Jan 02 23:00:52 2008 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Jan 02 23:00:54 2008 +0100
     1.3 @@ -750,11 +750,9 @@
     1.4  
     1.5  val _ =
     1.6    OuterSyntax.improper_command "Isabelle.command" "nested Isabelle command" K.control
     1.7 -    (P.position P.string :|-- (fn (str, pos) =>
     1.8 -      (case OuterSyntax.parse pos str of
     1.9 -        [transition] => Scan.succeed (K transition)
    1.10 -      | _ => Scan.fail_with (K "exactly one command expected"))
    1.11 -      handle ERROR msg => Scan.fail_with (K msg)));
    1.12 +    ((Scan.optional P.properties [] -- P.position P.string) :|-- (fn (props, arg) =>
    1.13 +      Scan.succeed (K (IsarCmd.nested_command props arg))
    1.14 +        handle ERROR msg => Scan.fail_with (K msg)));
    1.15  
    1.16  
    1.17