--- a/src/HOL/Tools/Function/induction_schema.ML Wed Dec 06 19:34:59 2017 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML Wed Dec 06 20:43:09 2017 +0100
@@ -140,7 +140,7 @@
end
fun mk_wf R (IndScheme {T, ...}) =
- HOLogic.Trueprop $ (Const (@{const_name wf}, mk_relT T --> HOLogic.boolT) $ R)
+ HOLogic.Trueprop $ (Const (\<^const_name>\<open>wf\<close>, mk_relT T --> HOLogic.boolT) $ R)
fun mk_ineqs R thesisn (IndScheme {T, cases, branches}) =
let
@@ -215,7 +215,7 @@
val ihyp = Logic.all_const T $ Abs ("z", T,
Logic.mk_implies
(HOLogic.mk_Trueprop (
- Const (@{const_name Set.member}, HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT)
+ Const (\<^const_name>\<open>Set.member\<close>, HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT)
$ (HOLogic.pair_const T T $ Bound 0 $ x)
$ R),
HOLogic.mk_Trueprop (P_comp $ Bound 0)))