--- a/src/HOL/Tools/Function/induction_schema.ML Thu Jul 01 16:54:42 2010 +0200
+++ b/src/HOL/Tools/Function/induction_schema.ML Thu Jul 01 16:54:42 2010 +0200
@@ -220,7 +220,7 @@
val ihyp = Term.all T $ Abs ("z", T,
Logic.mk_implies
(HOLogic.mk_Trueprop (
- Const ("op :", HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT)
+ Const (@{const_name Set.member}, 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)))