src/HOL/Tools/Function/induction_schema.ML
changeset 46217 7b19666f0e3d
parent 42495 1af81b70cf09
child 46467 39e412f9ffdf
     1.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Sat Jan 14 18:18:06 2012 +0100
     1.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Sat Jan 14 19:06:05 2012 +0100
     1.3 @@ -217,7 +217,7 @@
     1.4      val P_comp = mk_ind_goal thy branches
     1.5  
     1.6      (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
     1.7 -    val ihyp = Term.all T $ Abs ("z", T,
     1.8 +    val ihyp = Logic.all_const T $ Abs ("z", T,
     1.9        Logic.mk_implies
    1.10          (HOLogic.mk_Trueprop (
    1.11            Const (@{const_name Set.member}, HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT)