src/HOLCF/IOA/Modelcheck/MuIOA.thy

   let
     val sign = Thm.theory_of_cterm csubgoal;
     val subgoal = Thm.term_of csubgoal;
   in
  (let
-    val weak_case_congs = (map (#weak_case_cong o snd) o Symtab.dest o DatatypePackage.get_datatypes) sign;
+    val weak_case_congs = (map (#weak_case_cong o snd) o Symtab.dest o Datatype.get_datatypes) sign;
     val concl = Logic.strip_imp_concl subgoal;
     val ic_str = delete_ul_string(Syntax.string_of_term_global sign (IntC sign concl));
     val ia_str = delete_ul_string(Syntax.string_of_term_global sign (IntA sign concl));
 	val sc_str = delete_ul_string(Syntax.string_of_term_global sign (StartC sign concl));	
 	val sa_str = delete_ul_string(Syntax.string_of_term_global sign (StartA sign concl));