--- a/src/HOL/Tools/inductive.ML Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Tools/inductive.ML Fri Jan 04 23:22:53 2019 +0100
@@ -575,7 +575,7 @@
local
(*delete needless equality assumptions*)
-val refl_thin = Goal.prove_global @{theory HOL} [] [] \<^prop>\<open>\<And>P. a = a \<Longrightarrow> P \<Longrightarrow> P\<close>
+val refl_thin = Goal.prove_global \<^theory>\<open>HOL\<close> [] [] \<^prop>\<open>\<And>P. a = a \<Longrightarrow> P \<Longrightarrow> P\<close>
(fn {context = ctxt, ...} => assume_tac ctxt 1);
val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE];
fun elim_tac ctxt = REPEAT o eresolve_tac ctxt elim_rls;