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