1.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Jul 23 16:12:12 2011 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Jul 23 16:37:17 2011 +0200
     1.3 @@ -775,8 +775,8 @@
     1.4      (props_text :|-- (fn (pos, str) =>
     1.5        (case Outer_Syntax.parse pos str of
     1.6          [tr] => Scan.succeed (K tr)
     1.7 -      | _ => Scan.fail_with (K "exactly one command expected"))
     1.8 -      handle ERROR msg => Scan.fail_with (K msg)));
     1.9 +      | _ => Scan.fail_with (K (fn () => "exactly one command expected")))
    1.10 +      handle ERROR msg => Scan.fail_with (K (fn () => msg))));
    1.11  
    1.12  
    1.13