src/HOL/IsaMakefile

   Tools/Datatype/datatype_case.ML \
   Tools/Datatype/datatype_codegen.ML \
   Tools/Datatype/datatype_data.ML \
   Tools/Datatype/datatype_prop.ML \
   Tools/Datatype/datatype_realizer.ML \
+  Tools/Datatype/rep_datatype.ML \
   Tools/Function/context_tree.ML \
   Tools/Function/fun.ML \
   Tools/Function/function.ML \
   Tools/Function/function_common.ML \
   Tools/Function/function_core.ML \

   Tools/Metis/metis_translate.ML \
   Tools/abel_cancel.ML \
   Tools/arith_data.ML \
   Tools/cnf_funcs.ML \
   Tools/dseq.ML \
+  Tools/enriched_type.ML \
   Tools/inductive.ML \
   Tools/inductive_realizer.ML \
   Tools/inductive_set.ML \
   Tools/lambda_lifting.ML \
   Tools/lin_arith.ML \

   Tools/sat_funcs.ML \
   Tools/sat_solver.ML \
   Tools/split_rule.ML \
   Tools/try_methods.ML \
   Tools/typedef.ML \
-  Tools/enriched_type.ML \
   Transitive_Closure.thy \
   Typedef.thy \
   Wellfounded.thy
 
 $(OUT)/HOL-Plain: plain.ML $(PLAIN_DEPENDENCIES)