TFL/post.ML

        val {induction, rules, tcs} =
              proof_stage strict cs ss wfs theory
                {f = f, R = R, rules = rules,
                 full_pats_TCs = full_pats_TCs,
                 TCs = TCs}
-       val rules' = map (standard o Rulify.rulify_no_asm) (R.CONJUNCTS rules)
-   in  {induct = meta_outer (Rulify.rulify_no_asm (induction RS spec')),
+       val rules' = map (standard o ObjectLogic.rulify_no_asm) (R.CONJUNCTS rules)
+   in  {induct = meta_outer (ObjectLogic.rulify_no_asm (induction RS spec')),
         rules = ListPair.zip(rules', rows),
         tcs = (termination_goals rules') @ tcs}
    end
   handle U.ERR {mesg,func,module} =>
                error (mesg ^