src/Pure/Isar/isar_syn.ML
changeset 43947 9b00f09f7721
parent 43775 b361c7d184e7
child 44186 806f0ec1a43d
     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