src/HOL/Nominal/nominal_atoms.ML

   let
     
     val (_,thy1) = 
     fold_map (fn ak => fn thy => 
           let val dt = ((Binding.name ak, [], NoSyn), [(Binding.name ak, [@{typ nat}], NoSyn)])
-              val (dt_names, thy1) = Datatype.add_datatype Datatype_Aux.default_config [dt] thy;
+              val (dt_names, thy1) =
+                Old_Datatype.add_datatype Old_Datatype_Aux.default_config [dt] thy;
             
-              val injects = maps (#inject o Datatype_Data.the_info thy1) dt_names;
+              val injects = maps (#inject o Old_Datatype_Data.the_info thy1) dt_names;
               val ak_type = Type (Sign.intern_type thy1 ak,[])
               val ak_sign = Sign.intern_const thy1 ak 
               
               val inj_type = @{typ nat} --> ak_type
               val inj_on_type = inj_type --> @{typ "nat set"} --> @{typ bool}

                 (Free (swap_name, swapT) $ HOLogic.mk_prod (a,b) $ c,
                     cif $ HOLogic.mk_eq (a,c) $ b $ (cif $ HOLogic.mk_eq (b,c) $ a $ c)))
         val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c)
       in
         thy' |>
-        Primrec.add_primrec_global
+        Old_Primrec.add_primrec_global
           [(Binding.name swap_name, SOME swapT, NoSyn)]
           [(Attrib.empty_binding, def1)] ||>
         Sign.parent_path ||>>
         Global_Theory.add_defs_unchecked true
           [((Binding.name name, def2), [])] |>> (snd o fst)

         val def2 = HOLogic.mk_Trueprop (HOLogic.mk_eq
                    (prm $ mk_Cons x xs $ a,
                     Const (swap_name, swapT) $ x $ (prm $ xs $ a)));
       in
         thy' |>
-        Primrec.add_primrec_global
+        Old_Primrec.add_primrec_global
           [(Binding.name prm_name, SOME prmT, NoSyn)]
           [(Attrib.empty_binding, def1), (Attrib.empty_binding, def2)] ||>
         Sign.parent_path
       end) ak_names_types thy3;