src/ZF/Tools/datatype_package.ML

     val dom_sum =
       if sdom = "" then Ind_Syntax.data_domain coind (rec_tms, con_ty_lists)
       else read_i sdom;
   in
     thy
-    |> IsarThy.apply_theorems raw_monos
-    ||>> IsarThy.apply_theorems raw_type_intrs
-    ||>> IsarThy.apply_theorems raw_type_elims
+    |> IsarCmd.apply_theorems raw_monos
+    ||>> IsarCmd.apply_theorems raw_type_intrs
+    ||>> IsarCmd.apply_theorems raw_type_elims
     |-> (fn ((monos, type_intrs), type_elims) =>
           add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims))
   end;
 
 (* outer syntax *)