src/FOLP/IFOLP.thy

    apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *})
   done
 
 (*special cases for free variables P, Q, R, S -- up to 3 arguments*)
 
-ML_setup {*
+ML {*
   bind_thms ("pred_congs",
     flat (map (fn c =>
                map (fn th => read_instantiate [("P",c)] th)
                    [@{thm pred1_cong}, @{thm pred2_cong}, @{thm pred3_cong}])
                (explode"PQRS")))