1.1 --- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Tue Sep 09 17:51:07 2014 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Tue Sep 09 20:51:36 2014 +0200
     1.3 @@ -107,13 +107,13 @@
     1.4    "unique [] = True"
     1.5  | "unique (x # xs) = (xs\<langle>fst x\<rangle>\<^sub>? = \<bottom> \<and> unique xs)"
     1.6  
     1.7 -datatype type =
     1.8 +datatype_new type =
     1.9      TVar nat
    1.10    | Top
    1.11    | Fun type type    (infixr "\<rightarrow>" 200)
    1.12    | TyAll type type  ("(3\<forall><:_./ _)" [0, 10] 10)
    1.13  
    1.14 -datatype binding = VarB type | TVarB type
    1.15 +datatype_new binding = VarB type | TVarB type
    1.16  type_synonym env = "binding list"
    1.17  
    1.18  primrec is_TVarB :: "binding \<Rightarrow> bool"
    1.19 @@ -131,7 +131,7 @@
    1.20    "mapB f (VarB T) = VarB (f T)"
    1.21  | "mapB f (TVarB T) = TVarB (f T)"
    1.22  
    1.23 -datatype trm =
    1.24 +datatype_new trm =
    1.25      Var nat
    1.26    | Abs type trm   ("(3\<lambda>:_./ _)" [0, 10] 10)
    1.27    | TAbs type trm  ("(3\<lambda><:_./ _)" [0, 10] 10)