src/HOL/Statespace/state_fun.ML

 
 fun mkName (Type (T,args)) = implode (map mkName args) ^ mkUpper (Long_Name.base_name T)
   | mkName (TFree (x,_)) = mkUpper (Long_Name.base_name x)
   | mkName (TVar ((x,_),_)) = mkUpper (Long_Name.base_name x);
 
-fun is_datatype thy = is_some o Datatype_Data.get_info thy;
+fun is_datatype thy = is_some o Old_Datatype_Data.get_info thy;
 
 fun mk_map @{type_name List.list} = Syntax.const @{const_name List.map}
   | mk_map n = Syntax.const ("StateFun.map_" ^ Long_Name.base_name n);
 
 fun gen_constr_destr comp prfx thy (Type (T, [])) =