src/HOL/Tools/Function/induction_schema.ML
changeset 37677 c5a8b612e571
parent 36945 9bec62c10714
child 39756 6c8e83d94536
     1.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Thu Jul 01 16:54:42 2010 +0200
     1.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Thu Jul 01 16:54:42 2010 +0200
     1.3 @@ -220,7 +220,7 @@
     1.4      val ihyp = Term.all T $ Abs ("z", T,
     1.5        Logic.mk_implies
     1.6          (HOLogic.mk_Trueprop (
     1.7 -          Const ("op :", HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT) 
     1.8 +          Const (@{const_name Set.member}, HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT) 
     1.9            $ (HOLogic.pair_const T T $ Bound 0 $ x)
    1.10            $ R),
    1.11           HOLogic.mk_Trueprop (P_comp $ Bound 0)))