src/HOL/Inductive.thy
changeset 58306 117ba6cbe414
parent 58187 d2ddd401d74d
child 58815 fd3f893a40ea
     1.1 --- a/src/HOL/Inductive.thy	Thu Sep 11 18:54:36 2014 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Thu Sep 11 18:54:36 2014 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4    "inductive" "coinductive" "inductive_cases" "inductive_simps" :: thy_decl and
     1.5    "monos" and
     1.6    "print_inductives" :: diag and
     1.7 -  "rep_datatype" :: thy_goal and
     1.8 +  "old_rep_datatype" :: thy_goal and
     1.9    "primrec" :: thy_decl
    1.10  begin
    1.11