diff -r 27f3c10b0b50 -r 4cf66f21b764 src/HOL/Fun_Def.thy
--- a/src/HOL/Fun_Def.thy	Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Fun_Def.thy	Mon Dec 07 10:38:04 2015 +0100
@@ -223,7 +223,7 @@
 lemma wf_pair_less[simp]: "wf pair_less"
   by (auto simp: pair_less_def)
 
-text \<open>Introduction rules for @{text pair_less}/@{text pair_leq}\<close>
+text \<open>Introduction rules for \<open>pair_less\<close>/\<open>pair_leq\<close>\<close>
 lemma pair_leqI1: "a < b \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq"
   and pair_leqI2: "a \<le> b \<Longrightarrow> s \<le> t \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq"
   and pair_lessI1: "a < b  \<Longrightarrow> ((a, s), (b, t)) \<in> pair_less"
@@ -301,7 +301,7 @@
 ML_file "Tools/Function/scnp_reconstruct.ML"
 ML_file "Tools/Function/fun_cases.ML"
 
-ML_val -- "setup inactive"
+ML_val \<comment> "setup inactive"
 \<open>
   Context.theory_map (Function_Common.set_termination_prover
     (K (ScnpReconstruct.decomp_scnp_tac [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS])))