src/Pure/General/symbol_pos.ML
changeset 55709 4e5a83a46ded
parent 55107 1a29ea173bf9
child 55828 42ac3cfb89f6
     1.1 --- a/src/Pure/General/symbol_pos.ML	Mon Feb 24 10:17:29 2014 +0100
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Mon Feb 24 10:48:34 2014 +0100
     1.3 @@ -178,8 +178,8 @@
     1.4  fun cartouche_content syms =
     1.5    let
     1.6      fun err () =
     1.7 -      error ("Malformed text cartouche: " ^ quote (content syms) ^
     1.8 -        Position.here (Position.set_range (range syms)));
     1.9 +      error ("Malformed text cartouche: "
    1.10 +        ^ quote (content syms) ^ Position.here (#1 (range syms)));
    1.11    in
    1.12      (case syms of
    1.13        ("\\<open>", _) :: rest =>