src/HOL/Inductive.thy
changeset 45890 5f70aaecae26
parent 44860 56101fa00193
child 45891 d73605c829cc
--- a/src/HOL/Inductive.thy	Thu Dec 15 14:11:57 2011 +0100
+++ b/src/HOL/Inductive.thy	Thu Dec 15 17:37:14 2011 +0100
@@ -14,6 +14,7 @@
   "Tools/Datatype/datatype_case.ML"
   ("Tools/Datatype/datatype_abs_proofs.ML")
   ("Tools/Datatype/datatype_data.ML")
+  ("Tools/Datatype/rep_datatype.ML")
   ("Tools/primrec.ML")
   ("Tools/Datatype/datatype_codegen.ML")
 begin
@@ -279,6 +280,8 @@
 use "Tools/Datatype/datatype_data.ML"
 setup Datatype_Data.setup
 
+use "Tools/Datatype/rep_datatype.ML"
+
 use "Tools/Datatype/datatype_codegen.ML"
 setup Datatype_Codegen.setup