diff -r e9ab4ad7bd15 -r 23307fd33906 src/HOL/Data_Structures/Less_False.thy
--- a/src/HOL/Data_Structures/Less_False.thy	Thu Jan 11 13:48:17 2018 +0100
+++ b/src/HOL/Data_Structures/Less_False.thy	Fri Jan 12 14:08:53 2018 +0100
@@ -1,12 +1,12 @@
 (* Author: Tobias Nipkow *)
 
-section {* Improved Simproc for $<$ *}
+section \<open>Improved Simproc for $<$\<close>
 
 theory Less_False
 imports Main
 begin
 
-simproc_setup less_False ("(x::'a::order) < y") = {* fn _ => fn ctxt => fn ct =>
+simproc_setup less_False ("(x::'a::order) < y") = \<open>fn _ => fn ctxt => fn ct =>
   let
     fun prp t thm = Thm.full_prop_of thm aconv t;
 
@@ -26,6 +26,6 @@
          | SOME thm => NONE
       end;
   in prove_less_False (Thm.term_of ct) end
-*}
+\<close>
 
 end