--- a/src/HOL/Tools/Function/mutual.ML Wed Dec 06 19:34:59 2017 +0100
+++ b/src/HOL/Tools/Function/mutual.ML Wed Dec 06 20:43:09 2017 +0100
@@ -247,7 +247,7 @@
fun mutual_cases_rule ctxt cases_rule n ST (MutualPart {i, cargTs = Ts, ...}) =
let
val [P, x] =
- Variable.variant_frees ctxt [] [("P", @{typ bool}), ("x", HOLogic.mk_tupleT Ts)]
+ Variable.variant_frees ctxt [] [("P", \<^typ>\<open>bool\<close>), ("x", HOLogic.mk_tupleT Ts)]
|> map (Thm.cterm_of ctxt o Free);
val sumtree_inj = Thm.cterm_of ctxt (Sum_Tree.mk_inj ST n i (Thm.term_of x));