--- a/src/HOL/Decision_Procs/Ferrack.thy Tue Nov 10 14:18:41 2015 +0000
+++ b/src/HOL/Decision_Procs/Ferrack.thy Tue Nov 10 14:43:29 2015 +0000
@@ -7,7 +7,7 @@
"~~/src/HOL/Library/Code_Target_Numeral" "~~/src/HOL/Library/Old_Recdef"
begin
-section \<open>Quantifier elimination for @{text "\<real> (0, 1, +, <)"}\<close>
+section \<open>Quantifier elimination for \<open>\<real> (0, 1, +, <)\<close>\<close>
(*********************************************************************************)
(**** SHADOW SYNTAX AND SEMANTICS ****)