src/Pure/Thy/markdown.ML
changeset 62529 8b7bdfc09f3b
parent 61595 3591274c607e
child 62804 7b9c5416f30e
     1.1 --- a/src/Pure/Thy/markdown.ML	Sun Mar 06 13:19:19 2016 +0100
     1.2 +++ b/src/Pure/Thy/markdown.ML	Sun Mar 06 16:19:02 2016 +0100
     1.3 @@ -49,7 +49,7 @@
     1.4  
     1.5  val kinds = [("item", Itemize), ("enum", Enumerate), ("descr", Description)];
     1.6  
     1.7 -val is_control = member (op =) ["\\<^item>", "\\<^enum>", "\\<^descr>"];
     1.8 +val is_control = member (op =) ["\<^item>", "\<^enum>", "\<^descr>"];
     1.9  
    1.10  
    1.11  (* document lines *)