src/Pure/Isar/isar_syn.ML
changeset 25588 514ae4e4d164
parent 25585 19cd3474fdf3
child 25625 35e2aa8b8b03
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Dec 08 22:07:22 2007 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Dec 08 22:28:27 2007 +0100
     1.3 @@ -753,7 +753,7 @@
     1.4      (P.position P.string :|-- (fn (str, pos) =>
     1.5        (case OuterSyntax.parse pos str of
     1.6          [transition] => Scan.succeed (K transition)
     1.7 -      | _ => Scan.fail_with (K "exactly one nested command expected"))
     1.8 +      | _ => Scan.fail_with (K "exactly one command expected"))
     1.9        handle ERROR msg => Scan.fail_with (K ("malformed command\n" ^ msg))));
    1.10  
    1.11