src/Pure/Isar/element.ML

   let
     val thy = ProofContext.theory_of ctxt;
     val cert = Thm.cterm_of thy;
 
     val th = MetaSimplifier.norm_hhf raw_th;
-    val is_elim = ObjectLogic.is_elim th;
+    val is_elim = Object_Logic.is_elim th;
 
     val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body false ctxt);
     val prop = Thm.prop_of th';
     val (prems, concl) = Logic.strip_horn prop;
-    val concl_term = ObjectLogic.drop_judgment thy concl;
+    val concl_term = Object_Logic.drop_judgment thy concl;
 
     val fixes = fold_aterms (fn v as Free (x, T) =>
         if Variable.newly_fixed ctxt' ctxt x andalso not (v aconv concl_term)
         then insert (op =) (x, T) else I | _ => I) prop [] |> rev;
     val (assumes, cases) = take_suffix (fn prem =>