src/Pure/Thy/markdown.ML
changeset 62804 7b9c5416f30e
parent 62529 8b7bdfc09f3b
child 64357 e10fa8afc96c
     1.1 --- a/src/Pure/Thy/markdown.ML	Fri Apr 01 18:46:25 2016 +0200
     1.2 +++ b/src/Pure/Thy/markdown.ML	Fri Apr 01 18:56:31 2016 +0200
     1.3 @@ -86,7 +86,7 @@
     1.4    | (c, pos) :: _ =>
     1.5        error ("Bad blank character " ^ quote (ML_Syntax.print_char c) ^ Position.here pos));
     1.6  
     1.7 -fun is_space ((s, _): Symbol_Pos.T) = s = Symbol.space;
     1.8 +val is_space = Symbol.is_space o Symbol_Pos.symbol;
     1.9  val is_empty = forall (fn Antiquote.Text ss => forall is_space ss | _ => false);
    1.10  
    1.11  fun strip_spaces (Antiquote.Text ss :: rest) =