src/HOL/SPARK/Tools/spark_vcs.ML

 
 (** generate properties of enumeration types **)
 
 fun add_enum_type tyname tyname' thy =
   let
-    val {case_name, ...} = the (Datatype_Data.get_info thy tyname');
-    val cs = map Const (the (Datatype_Data.get_constrs thy tyname'));
+    val {case_name, ...} = the (Old_Datatype_Data.get_info thy tyname');
+    val cs = map Const (the (Old_Datatype_Data.get_constrs thy tyname'));
     val k = length cs;
     val T = Type (tyname', []);
     val p = Const (@{const_name pos}, T --> HOLogic.intT);
     val v = Const (@{const_name val}, HOLogic.intT --> T);
     val card = Const (@{const_name card},

       (HOLogic.mk_Trueprop (HOLogic.mk_eq
          (HOLogic.mk_UNIV T, HOLogic.mk_set T cs)))
       (fn _ =>
          rtac @{thm subset_antisym} 1 THEN
          rtac @{thm subsetI} 1 THEN
-         Datatype_Aux.exh_tac (K (#exhaust (Datatype_Data.the_info
+         Old_Datatype_Aux.exh_tac (K (#exhaust (Old_Datatype_Data.the_info
            (Proof_Context.theory_of lthy) tyname'))) 1 THEN
          ALLGOALS (asm_full_simp_tac lthy));
 
     val finite_UNIV = Goal.prove lthy [] []
       (HOLogic.mk_Trueprop (Const (@{const_name finite},

               let
                 val tyb = Binding.name s;
                 val tyname = Sign.full_name thy tyb
               in
                 (thy |>
-                 Datatype.add_datatype {strict = true, quiet = true}
+                 Old_Datatype.add_datatype {strict = true, quiet = true}
                    [((tyb, [], NoSyn),
                      map (fn s => (Binding.name s, [], NoSyn)) els)] |> snd |>
                  add_enum_type s tyname,
                  tyname)
               end
           | SOME (T as Type (tyname, []), cmap) =>
-              (case Datatype_Data.get_constrs thy tyname of
+              (case Old_Datatype_Data.get_constrs thy tyname of
                  NONE => assoc_ty_err thy T s "is not a datatype"
                | SOME cs =>
                    let val (prfx', _) = strip_prfx s
                    in
                      case check_enum (map (unprefix_pfun prfx') els)
                          (invert_map cmap cs) of
                        NONE => (thy, tyname)
                      | SOME msg => assoc_ty_err thy T s msg
                    end)
           | SOME (T, _) => assoc_ty_err thy T s "is not a datatype");
-        val cs = map Const (the (Datatype_Data.get_constrs thy' tyname));
+        val cs = map Const (the (Old_Datatype_Data.get_constrs thy' tyname));
       in
         ((fold (Symtab.update_new o apsnd (rpair s)) (els ~~ cs) tab,
           fold Name.declare els ctxt),
          thy')
       end

                type_map = Symtab.update_new (s, (T, cmap')) type_map,
                env = env}
                 handle Symtab.DUP _ => error ("SPARK type " ^ s ^
                   " already associated with type")) |>
         (fn thy' =>
-           case Datatype_Data.get_constrs thy' tyname of
+           case Old_Datatype_Data.get_constrs thy' tyname of
              NONE => (case get_record_info thy' T of
                NONE => thy'
              | SOME {fields, ...} =>
                  (check_mapping (assoc_ty_err thy' T s) "field"
                     cmap' (map fst fields);