diff -r 143f58bb34f9 -r 0909deb8059b src/HOL/Metis_Examples/Proxies.thy
--- a/src/HOL/Metis_Examples/Proxies.thy	Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/Metis_Examples/Proxies.thy	Thu May 26 17:51:22 2016 +0200
@@ -5,10 +5,10 @@
 rudimentary higher-order reasoning.
 *)
 
-section {*
+section \<open>
 Example that Exercises Metis's and Sledgehammer's Logical Symbol Proxies for
 Rudimentary Higher-Order Reasoning.
-*}
+\<close>
 
 theory Proxies
 imports Type_Encodings
@@ -17,7 +17,7 @@
 sledgehammer_params [prover = spass, fact_filter = mepo, timeout = 30, preplay_timeout = 0,
   dont_minimize]
 
-text {* Extensionality and set constants *}
+text \<open>Extensionality and set constants\<close>
 
 lemma plus_1_not_0: "n + (1::nat) \<noteq> 0"
 by simp
@@ -57,7 +57,7 @@
 sledgehammer [expect = some]
 by (metis_exhaust B_def C_def int_le_0_imp_le_1 predicate1I)
 
-text {* Proxies for logical constants *}
+text \<open>Proxies for logical constants\<close>
 
 lemma "id (op =) x x"
 sledgehammer [type_enc = erased, expect = none] (id_apply)