src/HOL/Tools/TFL/post.ML

        val {induction, rules, tcs} =
              proof_stage strict cs ss wfs thy
                {f = f, R = R, rules = rules,
                 full_pats_TCs = full_pats_TCs,
                 TCs = TCs}
-       val rules' = map (Drule.export_without_context o ObjectLogic.rulify_no_asm)
+       val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm)
                         (R.CONJUNCTS rules)
-         in  {induct = meta_outer (ObjectLogic.rulify_no_asm (induction RS spec')),
+         in  {induct = meta_outer (Object_Logic.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 ^

   fun solve_eq (th, [], i) = 
         error "derive_init_eqs: missing rules"
     | solve_eq (th, [a], i) = [(a, i)]
     | solve_eq (th, splitths as (_ :: _), i) = 
       (writeln "Proving unsplit equation...";
-      [((Drule.export_without_context o ObjectLogic.rulify_no_asm)
+      [((Drule.export_without_context o Object_Logic.rulify_no_asm)
           (CaseSplit.splitto splitths th), i)])
       (* if there's an error, pretend nothing happened with this definition 
          We should probably print something out so that the user knows...? *)
       handle ERROR s => 
              (warning ("recdef (solve_eq): " ^ s); map (fn x => (x,i)) splitths);