src/HOL/Inductive.thy

 imports Complete_Lattices Ctr_Sugar
 keywords
   "inductive" "coinductive" "inductive_cases" "inductive_simps" :: thy_decl and
   "monos" and
   "print_inductives" :: diag and
-  "rep_datatype" :: thy_goal and
+  "old_rep_datatype" :: thy_goal and
   "primrec" :: thy_decl
 begin
 
 subsection {* Least and greatest fixed points *}