changeset 46217 | 7b19666f0e3d |
parent 42495 | 1af81b70cf09 |
child 46467 | 39e412f9ffdf |
--- a/src/HOL/Tools/Function/induction_schema.ML Sat Jan 14 18:18:06 2012 +0100 +++ b/src/HOL/Tools/Function/induction_schema.ML Sat Jan 14 19:06:05 2012 +0100 @@ -217,7 +217,7 @@ val P_comp = mk_ind_goal thy branches (* Inductive Hypothesis: !!z. (z,x):R ==> P z *) - val ihyp = Term.all T $ Abs ("z", T, + 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)