src/HOL/Tools/Function/induction_schema.ML

     val cert = cterm_of thy
 
     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) 
           $ (HOLogic.pair_const T T $ Bound 0 $ x)
           $ R),