1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Fri Aug 30 15:36:00 2013 +0200
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Fri Aug 30 15:54:23 2013 +0200
     1.3 @@ -246,10 +246,11 @@
     1.4  simplest recursive type: copy of the natural numbers:
     1.5  *}
     1.6  
     1.7 +    datatype_new nat = Zero | Suc nat
     1.8  (*<*)
     1.9 -    (* FIXME: remove "rep_compat" once "datatype_new" is integrated with "fun" *)
    1.10 +    (* FIXME: remove once "datatype_new" is integrated with "fun" *)
    1.11 +    datatype_new_compat nat
    1.12  (*>*)
    1.13 -    datatype_new (*<*)(rep_compat) (*>*)nat = Zero | Suc nat
    1.14  
    1.15  text {*
    1.16  lists were shown in the introduction; terminated lists are a variant:
    1.17 @@ -638,16 +639,12 @@
    1.18  we don't like the confusing name @{const nth}:
    1.19  *}
    1.20  
    1.21 -    (* FIXME *)
    1.22 -    primrec_new_notyet at :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" where
    1.23 +    primrec_new at :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" where
    1.24        "at (a # as) j =
    1.25           (case j of
    1.26              Zero \<Rightarrow> a
    1.27            | Suc j' \<Rightarrow> at as j')"
    1.28  
    1.29 -    primrec_new at :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" where
    1.30 -      "at (a # as) j = nat_case a (at as) j"
    1.31 -
    1.32      primrec_new tfold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) tlist \<Rightarrow> 'b" where
    1.33        "tfold _ (TNil b) = b" |
    1.34        "tfold f (TCons a as) = f a (tfold f as)"
    1.35 @@ -674,11 +671,6 @@
    1.36  Mutual recursion is be possible within a single type, but currently only using fun:
    1.37  *}
    1.38  
    1.39 -(*<*)
    1.40 -    (* FIXME: remove hack once "primrec_new" is in place *)
    1.41 -    rep_datatype Zero Suc
    1.42 -    by (erule nat.induct, assumption) auto
    1.43 -(*>*)
    1.44      fun
    1.45        even :: "nat \<Rightarrow> bool" and
    1.46        odd :: "nat \<Rightarrow> bool"