bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)

--- a/src/HOL/Datatype.thy	Wed Nov 25 09:14:28 2009 +0100
+++ b/src/HOL/Datatype.thy	Wed Nov 25 11:16:57 2009 +0100
@@ -8,9 +8,15 @@
 header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *}
 
 theory Datatype
-imports Nat Product_Type
+imports Product_Type Sum_Type Nat
+uses
+  ("Tools/Datatype/datatype_rep_proofs.ML")
+  ("Tools/inductive_realizer.ML")
+  ("Tools/Datatype/datatype_realizer.ML")
 begin
 
+subsection {* The datatype universe *}
+
 typedef (Node)
   ('a,'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}"
     --{*it is a subtype of @{text "(nat=>'b+nat) * ('a+nat)"}*}
@@ -513,75 +519,12 @@
 hide (open) type node item
 hide (open) const Push Node Atom Leaf Numb Lim Split Case
 
-
-section {* Datatypes *}
-
-subsection {* Representing sums *}
-
-rep_datatype (sum) Inl Inr
-proof -
-  fix P
-  fix s :: "'a + 'b"
-  assume x: "\<And>x\<Colon>'a. P (Inl x)" and y: "\<And>y\<Colon>'b. P (Inr y)"
-  then show "P s" by (auto intro: sumE [of s])
-qed simp_all
-
-lemma sum_case_KK[simp]: "sum_case (%x. a) (%x. a) = (%x. a)"
-  by (rule ext) (simp split: sum.split)
-
-lemma surjective_sum: "sum_case (%x::'a. f (Inl x)) (%y::'b. f (Inr y)) s = f(s)"
-  apply (rule_tac s = s in sumE)
-   apply (erule ssubst)
-   apply (rule sum.cases(1))
-  apply (erule ssubst)
-  apply (rule sum.cases(2))
-  done
-
-lemma sum_case_weak_cong: "s = t ==> sum_case f g s = sum_case f g t"
-  -- {* Prevents simplification of @{text f} and @{text g}: much faster. *}
-  by simp
+use "Tools/Datatype/datatype_rep_proofs.ML"
 
-lemma sum_case_inject:
-  "sum_case f1 f2 = sum_case g1 g2 ==> (f1 = g1 ==> f2 = g2 ==> P) ==> P"
-proof -
-  assume a: "sum_case f1 f2 = sum_case g1 g2"
-  assume r: "f1 = g1 ==> f2 = g2 ==> P"
-  show P
-    apply (rule r)
-     apply (rule ext)
-     apply (cut_tac x = "Inl x" in a [THEN fun_cong], simp)
-    apply (rule ext)
-    apply (cut_tac x = "Inr x" in a [THEN fun_cong], simp)
-    done
-qed
-
-constdefs
-  Suml :: "('a => 'c) => 'a + 'b => 'c"
-  "Suml == (%f. sum_case f undefined)"
-
-  Sumr :: "('b => 'c) => 'a + 'b => 'c"
-  "Sumr == sum_case undefined"
+use "Tools/inductive_realizer.ML"
+setup InductiveRealizer.setup
 
-lemma [code]:
-  "Suml f (Inl x) = f x"
-  by (simp add: Suml_def)
-
-lemma [code]:
-  "Sumr f (Inr x) = f x"
-  by (simp add: Sumr_def)
-
-lemma Suml_inject: "Suml f = Suml g ==> f = g"
-  by (unfold Suml_def) (erule sum_case_inject)
-
-lemma Sumr_inject: "Sumr f = Sumr g ==> f = g"
-  by (unfold Sumr_def) (erule sum_case_inject)
-
-primrec Projl :: "'a + 'b => 'a"
-where Projl_Inl: "Projl (Inl x) = x"
-
-primrec Projr :: "'a + 'b => 'b"
-where Projr_Inr: "Projr (Inr x) = x"
-
-hide (open) const Suml Sumr Projl Projr
+use "Tools/Datatype/datatype_realizer.ML"
+setup DatatypeRealizer.setup
 
 end

--- a/src/HOL/Inductive.thy	Wed Nov 25 09:14:28 2009 +0100
+++ b/src/HOL/Inductive.thy	Wed Nov 25 11:16:57 2009 +0100
@@ -5,16 +5,15 @@
 header {* Knaster-Tarski Fixpoint Theorem and inductive definitions *}
 
 theory Inductive 
-imports Lattices Sum_Type
+imports Complete_Lattice
 uses
   ("Tools/inductive.ML")
   "Tools/dseq.ML"
   ("Tools/inductive_codegen.ML")
-  ("Tools/Datatype/datatype_aux.ML")
-  ("Tools/Datatype/datatype_prop.ML")
-  ("Tools/Datatype/datatype_rep_proofs.ML")
+  "Tools/Datatype/datatype_aux.ML"
+  "Tools/Datatype/datatype_prop.ML"
+  "Tools/Datatype/datatype_case.ML"
   ("Tools/Datatype/datatype_abs_proofs.ML")
-  ("Tools/Datatype/datatype_case.ML")
   ("Tools/Datatype/datatype.ML")
   ("Tools/old_primrec.ML")
   ("Tools/primrec.ML")
@@ -282,11 +281,7 @@
 
 text {* Package setup. *}
 
-use "Tools/Datatype/datatype_aux.ML"
-use "Tools/Datatype/datatype_prop.ML"
-use "Tools/Datatype/datatype_rep_proofs.ML"
 use "Tools/Datatype/datatype_abs_proofs.ML"
-use "Tools/Datatype/datatype_case.ML"
 use "Tools/Datatype/datatype.ML"
 setup Datatype.setup
 

--- a/src/HOL/Product_Type.thy	Wed Nov 25 09:14:28 2009 +0100
+++ b/src/HOL/Product_Type.thy	Wed Nov 25 11:16:57 2009 +0100
@@ -6,12 +6,10 @@
 header {* Cartesian products *}
 
 theory Product_Type
-imports Inductive
+imports Typedef Inductive Fun
 uses
   ("Tools/split_rule.ML")
   ("Tools/inductive_set.ML")
-  ("Tools/inductive_realizer.ML")
-  ("Tools/Datatype/datatype_realizer.ML")
 begin
 
 subsection {* @{typ bool} is a datatype *}
@@ -1195,16 +1193,7 @@
 val unit_eq = thm "unit_eq";
 *}
 
-
-subsection {* Further inductive packages *}
-
-use "Tools/inductive_realizer.ML"
-setup InductiveRealizer.setup
-
 use "Tools/inductive_set.ML"
 setup Inductive_Set.setup
 
-use "Tools/Datatype/datatype_realizer.ML"
-setup DatatypeRealizer.setup
-
 end

--- a/src/HOL/Tools/Datatype/datatype.ML	Wed Nov 25 09:14:28 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Wed Nov 25 11:16:57 2009 +0100
@@ -7,10 +7,9 @@
 signature DATATYPE =
 sig
   include DATATYPE_COMMON
-  val add_datatype : config -> string list -> (string list * binding * mixfix *
-    (binding * typ list * mixfix) list) list -> theory -> string list * theory
-  val datatype_cmd : string list -> (string list * binding * mixfix *
-    (binding * string list * mixfix) list) list -> theory -> theory
+  val derive_datatype_props : config -> string list -> string list option
+    -> descr list -> (string * sort) list -> thm -> thm list list -> thm list list
+    -> theory -> string list * theory
   val rep_datatype : config -> (string list -> Proof.context -> Proof.context)
     -> string list option -> term list -> theory -> Proof.state
   val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state
@@ -30,6 +29,8 @@
     (term * term) list -> term * (term * (int * bool)) list
   val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
   val read_typ: theory -> string -> (string * sort) list -> typ * (string * sort) list
+  val cert_typ: theory -> typ -> (string * sort) list -> typ * (string * sort) list
+  val mk_case_names_induct: descr -> attribute
   val setup: theory -> theory
 end;
 
@@ -442,89 +443,6 @@
 
 
 
-(** definitional introduction of datatypes **)
-
-fun gen_add_datatype prep_typ config new_type_names dts thy =
-  let
-    val _ = Theory.requires thy "Datatype" "datatype definitions";
-
-    (* this theory is used just for parsing *)
-    val tmp_thy = thy |>
-      Theory.copy |>
-      Sign.add_types (map (fn (tvs, tname, mx, _) =>
-        (tname, length tvs, mx)) dts);
-
-    val (tyvars, _, _, _)::_ = dts;
-    val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
-      let val full_tname = Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname)
-      in
-        (case duplicates (op =) tvs of
-          [] =>
-            if eq_set (op =) (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
-            else error ("Mutually recursive datatypes must have same type parameters")
-        | dups => error ("Duplicate parameter(s) for datatype " ^ quote (Binding.str_of tname) ^
-            " : " ^ commas dups))
-      end) dts);
-    val dt_names = map fst new_dts;
-
-    val _ =
-      (case duplicates (op =) (map fst new_dts) @ duplicates (op =) new_type_names of
-        [] => ()
-      | dups => error ("Duplicate datatypes: " ^ commas dups));
-
-    fun prep_dt_spec ((tvs, tname, mx, constrs), tname') (dts', constr_syntax, sorts, i) =
-      let
-        fun prep_constr (cname, cargs, mx') (constrs, constr_syntax', sorts') =
-          let
-            val (cargs', sorts'') = fold_map (prep_typ tmp_thy) cargs sorts';
-            val _ =
-              (case subtract (op =) tvs (fold (curry OldTerm.add_typ_tfree_names) cargs' []) of
-                [] => ()
-              | vs => error ("Extra type variables on rhs: " ^ commas vs))
-          in (constrs @ [(Sign.full_name_path tmp_thy tname'
-                  (Binding.map_name (Syntax.const_name mx') cname),
-                   map (dtyp_of_typ new_dts) cargs')],
-              constr_syntax' @ [(cname, mx')], sorts'')
-          end handle ERROR msg => cat_error msg
-           ("The error above occured in constructor " ^ quote (Binding.str_of cname) ^
-            " of datatype " ^ quote (Binding.str_of tname));
-
-        val (constrs', constr_syntax', sorts') =
-          fold prep_constr constrs ([], [], sorts)
-
-      in
-        case duplicates (op =) (map fst constrs') of
-           [] =>
-             (dts' @ [(i, (Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname),
-                map DtTFree tvs, constrs'))],
-              constr_syntax @ [constr_syntax'], sorts', i + 1)
-         | dups => error ("Duplicate constructors " ^ commas dups ^
-             " in datatype " ^ quote (Binding.str_of tname))
-      end;
-
-    val (dts', constr_syntax, sorts', i) =
-      fold prep_dt_spec (dts ~~ new_type_names) ([], [], [], 0);
-    val sorts = sorts' @ (map (rpair (Sign.defaultS tmp_thy)) (subtract (op =) (map fst sorts') tyvars));
-    val dt_info = get_all thy;
-    val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
-    val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
-      if #strict config then error ("Nonemptiness check failed for datatype " ^ s)
-      else raise exn;
-
-    val _ = message config ("Constructing datatype(s) " ^ commas_quote new_type_names);
-    val ((inject, distinct, induct), thy') = thy |>
-      DatatypeRepProofs.representation_proofs config dt_info new_type_names descr sorts
-        types_syntax constr_syntax (mk_case_names_induct (flat descr));
-  in
-    derive_datatype_props config dt_names (SOME new_type_names) descr sorts
-      induct inject distinct thy'
-  end;
-
-val add_datatype = gen_add_datatype cert_typ;
-val datatype_cmd = snd ooo gen_add_datatype read_typ default_config;
-
-
-
 (** package setup **)
 
 (* setup theory *)
@@ -540,27 +458,9 @@
 
 structure P = OuterParse and K = OuterKeyword
 
-fun prep_datatype_decls args =
-  let
-    val names = map
-      (fn ((((NONE, _), t), _), _) => Binding.name_of t | ((((SOME t, _), _), _), _) => t) args;
-    val specs = map (fn ((((_, vs), t), mx), cons) =>
-      (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
-  in (names, specs) end;
-
-val parse_datatype_decl =
-  (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_infix --
-    (P.$$$ "=" |-- P.enum1 "|" (P.binding -- Scan.repeat P.typ -- P.opt_mixfix)));
-
-val parse_datatype_decls = P.and_list1 parse_datatype_decl >> prep_datatype_decls;
-
 in
 
 val _ =
-  OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl
-    (parse_datatype_decls >> (fn (names, specs) => Toplevel.theory (datatype_cmd names specs)));
-
-val _ =
   OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_goal
     (Scan.option (P.$$$ "(" |-- Scan.repeat1 P.name --| P.$$$ ")") -- Scan.repeat1 P.term
       >> (fn (alt_names, ts) => Toplevel.print

--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Wed Nov 25 09:14:28 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Wed Nov 25 11:16:57 2009 +0100
@@ -1,8 +1,7 @@
 (*  Title:      HOL/Tools/datatype_rep_proofs.ML
     Author:     Stefan Berghofer, TU Muenchen
 
-Definitional introduction of datatypes
-Proof of characteristic theorems:
+Definitional introduction of datatypes with proof of characteristic theorems:
 
  - injectivity of constructors
  - distinctness of constructors
@@ -12,52 +11,56 @@
 signature DATATYPE_REP_PROOFS =
 sig
   include DATATYPE_COMMON
-  val representation_proofs : config -> info Symtab.table ->
-    string list -> descr list -> (string * sort) list ->
-      (binding * mixfix) list -> (binding * mixfix) list list -> attribute
-        -> theory -> (thm list list * thm list list * thm) * theory
+  val add_datatype : config -> string list -> (string list * binding * mixfix *
+    (binding * typ list * mixfix) list) list -> theory -> string list * theory
+  val datatype_cmd : string list -> (string list * binding * mixfix *
+    (binding * string list * mixfix) list) list -> theory -> theory
 end;
 
 structure DatatypeRepProofs : DATATYPE_REP_PROOFS =
 struct
 
+(** auxiliary **)
+
 open DatatypeAux;
 
 val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
 
 val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
 
-
-(** theory context references **)
-
 fun exh_thm_of (dt_info : info Symtab.table) tname =
   #exhaust (the (Symtab.lookup dt_info tname));
 
-(******************************************************************************)
+val node_name = @{type_name "Datatype.node"};
+val In0_name = @{const_name "Datatype.In0"};
+val In1_name = @{const_name "Datatype.In1"};
+val Scons_name = @{const_name "Datatype.Scons"};
+val Leaf_name = @{const_name "Datatype.Leaf"};
+val Numb_name = @{const_name "Datatype.Numb"};
+val Lim_name = @{const_name "Datatype.Lim"};
+val Suml_name = @{const_name "Sum_Type.Suml"};
+val Sumr_name = @{const_name "Sum_Type.Sumr"};
+
+val In0_inject = @{thm In0_inject};
+val In1_inject = @{thm In1_inject};
+val Scons_inject = @{thm Scons_inject};
+val Leaf_inject = @{thm Leaf_inject};
+val In0_eq = @{thm In0_eq};
+val In1_eq = @{thm In1_eq};
+val In0_not_In1 = @{thm In0_not_In1};
+val In1_not_In0 = @{thm In1_not_In0};
+val Lim_inject = @{thm Lim_inject};
+val Suml_inject = @{thm Suml_inject};
+val Sumr_inject = @{thm Sumr_inject};
+
+
+
+(** proof of characteristic theorems **)
 
 fun representation_proofs (config : config) (dt_info : info Symtab.table)
       new_type_names descr sorts types_syntax constr_syntax case_names_induct thy =
   let
-    val Datatype_thy = ThyInfo.the_theory "Datatype" thy;
-    val node_name = "Datatype.node";
-    val In0_name = "Datatype.In0";
-    val In1_name = "Datatype.In1";
-    val Scons_name = "Datatype.Scons";
-    val Leaf_name = "Datatype.Leaf";
-    val Numb_name = "Datatype.Numb";
-    val Lim_name = "Datatype.Lim";
-    val Suml_name = "Datatype.Suml";
-    val Sumr_name = "Datatype.Sumr";
-
-    val [In0_inject, In1_inject, Scons_inject, Leaf_inject,
-         In0_eq, In1_eq, In0_not_In1, In1_not_In0,
-         Lim_inject, Suml_inject, Sumr_inject] = map (PureThy.get_thm Datatype_thy)
-          ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject",
-           "In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0",
-           "Lim_inject", "Suml_inject", "Sumr_inject"];
-
     val descr' = flat descr;
-
     val big_name = space_implode "_" new_type_names;
     val thy1 = Sign.add_path big_name thy;
     val big_rec_name = big_name ^ "_rep_set";
@@ -83,7 +86,7 @@
     val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT, branchT]));
     val UnivT = HOLogic.mk_setT Univ_elT;
     val UnivT' = Univ_elT --> HOLogic.boolT;
-    val Collect = Const ("Collect", UnivT' --> UnivT);
+    val Collect = Const (@{const_name Collect}, UnivT' --> UnivT);
 
     val In0 = Const (In0_name, Univ_elT --> Univ_elT);
     val In1 = Const (In1_name, Univ_elT --> Univ_elT);
@@ -100,9 +103,9 @@
               val Type (_, [T1, T2]) = T
           in
             if i <= n2 then
-              Const ("Sum_Type.Inl", T1 --> T) $ (mk_inj' T1 n2 i)
+              Const (@{const_name "Sum_Type.Inl"}, T1 --> T) $ (mk_inj' T1 n2 i)
             else
-              Const ("Sum_Type.Inr", T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
+              Const (@{const_name "Sum_Type.Inr"}, T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
           end
       in mk_inj' sumT (length leafTs) (1 + find_index (fn T'' => T'' = T') leafTs)
       end;
@@ -629,4 +632,123 @@
     ((constr_inject', distinct_thms', dt_induct'), thy7)
   end;
 
+
+
+(** definitional introduction of datatypes **)
+
+fun gen_add_datatype prep_typ config new_type_names dts thy =
+  let
+    val _ = Theory.requires thy "Datatype" "datatype definitions";
+
+    (* this theory is used just for parsing *)
+    val tmp_thy = thy |>
+      Theory.copy |>
+      Sign.add_types (map (fn (tvs, tname, mx, _) =>
+        (tname, length tvs, mx)) dts);
+
+    val (tyvars, _, _, _)::_ = dts;
+    val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
+      let val full_tname = Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname)
+      in
+        (case duplicates (op =) tvs of
+          [] =>
+            if eq_set (op =) (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
+            else error ("Mutually recursive datatypes must have same type parameters")
+        | dups => error ("Duplicate parameter(s) for datatype " ^ quote (Binding.str_of tname) ^
+            " : " ^ commas dups))
+      end) dts);
+    val dt_names = map fst new_dts;
+
+    val _ =
+      (case duplicates (op =) (map fst new_dts) @ duplicates (op =) new_type_names of
+        [] => ()
+      | dups => error ("Duplicate datatypes: " ^ commas dups));
+
+    fun prep_dt_spec (tvs, tname, mx, constrs) tname' (dts', constr_syntax, sorts, i) =
+      let
+        fun prep_constr (cname, cargs, mx') (constrs, constr_syntax', sorts') =
+          let
+            val (cargs', sorts'') = fold_map (prep_typ tmp_thy) cargs sorts';
+            val _ =
+              (case subtract (op =) tvs (fold (curry OldTerm.add_typ_tfree_names) cargs' []) of
+                [] => ()
+              | vs => error ("Extra type variables on rhs: " ^ commas vs))
+          in (constrs @ [(Sign.full_name_path tmp_thy tname'
+                  (Binding.map_name (Syntax.const_name mx') cname),
+                   map (dtyp_of_typ new_dts) cargs')],
+              constr_syntax' @ [(cname, mx')], sorts'')
+          end handle ERROR msg => cat_error msg
+           ("The error above occured in constructor " ^ quote (Binding.str_of cname) ^
+            " of datatype " ^ quote (Binding.str_of tname));
+
+        val (constrs', constr_syntax', sorts') =
+          fold prep_constr constrs ([], [], sorts)
+
+      in
+        case duplicates (op =) (map fst constrs') of
+           [] =>
+             (dts' @ [(i, (Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname),
+                map DtTFree tvs, constrs'))],
+              constr_syntax @ [constr_syntax'], sorts', i + 1)
+         | dups => error ("Duplicate constructors " ^ commas dups ^
+             " in datatype " ^ quote (Binding.str_of tname))
+      end;
+
+    val (dts', constr_syntax, sorts', i) =
+      fold2 prep_dt_spec dts new_type_names ([], [], [], 0);
+    val sorts = sorts' @ map (rpair (Sign.defaultS tmp_thy)) (subtract (op =) (map fst sorts') tyvars);
+    val dt_info = Datatype.get_all thy;
+    val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
+    val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
+      if #strict config then error ("Nonemptiness check failed for datatype " ^ s)
+      else raise exn;
+
+    val _ = message config ("Constructing datatype(s) " ^ commas_quote new_type_names);
+
+  in
+    thy
+    |> representation_proofs config dt_info new_type_names descr sorts
+        types_syntax constr_syntax (Datatype.mk_case_names_induct (flat descr))
+    |-> (fn (inject, distinct, induct) => Datatype.derive_datatype_props
+        config dt_names (SOME new_type_names) descr sorts
+        induct inject distinct)
+  end;
+
+val add_datatype = gen_add_datatype Datatype.cert_typ;
+val datatype_cmd = snd ooo gen_add_datatype Datatype.read_typ default_config;
+
+local
+
+structure P = OuterParse and K = OuterKeyword
+
+fun prep_datatype_decls args =
+  let
+    val names = map
+      (fn ((((NONE, _), t), _), _) => Binding.name_of t | ((((SOME t, _), _), _), _) => t) args;
+    val specs = map (fn ((((_, vs), t), mx), cons) =>
+      (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
+  in (names, specs) end;
+
+val parse_datatype_decl =
+  (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_infix --
+    (P.$$$ "=" |-- P.enum1 "|" (P.binding -- Scan.repeat P.typ -- P.opt_mixfix)));
+
+val parse_datatype_decls = P.and_list1 parse_datatype_decl >> prep_datatype_decls;
+
+in
+
+val _ =
+  OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl
+    (parse_datatype_decls >> (fn (names, specs) => Toplevel.theory (datatype_cmd names specs)));
+
 end;
+
+end;
+
+structure Datatype =
+struct
+
+open Datatype;
+open DatatypeRepProofs;
+
+end;