# HG changeset patch
# User haftmann
# Date 1245604171 -7200
# Node ID 5fb12f859de691bebabf05850f2bab17b437f71b
# Parent  ec013c3ade5a48d41db5299e66662673fa1fadc4# Parent  7b9b9ba532caad091254d7dd19cd5227e8897c93
merged

diff -r ec013c3ade5a -r 5fb12f859de6 src/HOL/Nominal/nominal.ML
--- a/src/HOL/Nominal/nominal.ML	Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOL/Nominal/nominal.ML	Sun Jun 21 19:09:31 2009 +0200
@@ -6,7 +6,7 @@
 
 signature NOMINAL =
 sig
-  val add_nominal_datatype : DatatypeAux.datatype_config -> string list ->
+  val add_nominal_datatype : Datatype.config -> string list ->
     (string list * bstring * mixfix *
       (bstring * string list * mixfix) list) list -> theory -> theory
   type descr
@@ -2084,7 +2084,7 @@
     val names = map (fn ((((NONE, _), t), _), _) => 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 add_nominal_datatype DatatypeAux.default_datatype_config names specs end;
+  in add_nominal_datatype Datatype.default_config names specs end;
 
 val _ =
   OuterSyntax.command "nominal_datatype" "define inductive datatypes" K.thy_decl
diff -r ec013c3ade5a -r 5fb12f859de6 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Sun Jun 21 19:09:31 2009 +0200
@@ -102,7 +102,7 @@
     fold_map (fn ak => fn thy => 
           let val dt = ([], Binding.name ak, NoSyn, [(Binding.name ak, [@{typ nat}], NoSyn)])
               val ({inject,case_thms,...},thy1) = Datatype.add_datatype
-                DatatypeAux.default_datatype_config [ak] [dt] thy
+                Datatype.default_config [ak] [dt] thy
               val inject_flat = flat inject
               val ak_type = Type (Sign.intern_type thy1 ak,[])
               val ak_sign = Sign.intern_const thy1 ak 
diff -r ec013c3ade5a -r 5fb12f859de6 src/HOL/Tools/datatype_package/datatype.ML
--- a/src/HOL/Tools/datatype_package/datatype.ML	Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype.ML	Sun Jun 21 19:09:31 2009 +0200
@@ -6,26 +6,7 @@
 
 signature DATATYPE =
 sig
-  type datatype_config = DatatypeAux.datatype_config
-  type datatype_info = DatatypeAux.datatype_info
-  type descr = DatatypeAux.descr
-  val get_datatypes : theory -> datatype_info Symtab.table
-  val get_datatype : theory -> string -> datatype_info option
-  val the_datatype : theory -> string -> datatype_info
-  val datatype_of_constr : theory -> string -> datatype_info option
-  val datatype_of_case : theory -> string -> datatype_info option
-  val the_datatype_spec : theory -> string -> (string * sort) list * (string * typ list) list
-  val the_datatype_descr : theory -> string list
-    -> descr * (string * sort) list * string list
-      * (string list * string list) * (typ list * typ list)
-  val get_datatype_constrs : theory -> string -> (string * typ) list option
-  val distinct_simproc : simproc
-  val make_case :  Proof.context -> bool -> string list -> term ->
-    (term * term) list -> term * (term * (int * bool)) list
-  val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
-  val read_typ: theory ->
-    (typ list * (string * sort) list) * string -> typ list * (string * sort) list
-  val interpretation : (datatype_config -> string list -> theory -> theory) -> theory -> theory
+  include DATATYPE_COMMON
   type rules = {distinct : thm list list,
     inject : thm list list,
     exhaustion : thm list,
@@ -34,15 +15,31 @@
     split_thms : (thm * thm) list,
     induction : thm,
     simps : thm list}
-  val rep_datatype : datatype_config -> (rules -> Proof.context -> Proof.context)
-    -> string list option -> term list -> theory -> Proof.state;
-  val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state
-  val add_datatype : datatype_config -> string list -> (string list * binding * mixfix *
+  val add_datatype : config -> string list -> (string list * binding * mixfix *
     (binding * typ list * mixfix) list) list -> theory -> rules * theory
-  val add_datatype_cmd : string list -> (string list * binding * mixfix *
-    (binding * string list * mixfix) list) list -> theory -> rules * theory
+  val datatype_cmd : string list -> (string list * binding * mixfix *
+    (binding * string list * mixfix) list) list -> theory -> theory
+  val rep_datatype : config -> (rules -> Proof.context -> Proof.context)
+    -> string list option -> term list -> theory -> Proof.state
+  val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state
+  val get_datatypes : theory -> info Symtab.table
+  val get_datatype : theory -> string -> info option
+  val the_datatype : theory -> string -> info
+  val datatype_of_constr : theory -> string -> info option
+  val datatype_of_case : theory -> string -> info option
+  val the_datatype_spec : theory -> string -> (string * sort) list * (string * typ list) list
+  val the_datatype_descr : theory -> string list
+    -> descr * (string * sort) list * string list
+      * (string list * string list) * (typ list * typ list)
+  val get_datatype_constrs : theory -> string -> (string * typ) list option
+  val interpretation : (config -> string list -> theory -> theory) -> theory -> theory
+  val distinct_simproc : simproc
+  val make_case :  Proof.context -> bool -> string list -> term ->
+    (term * term) list -> term * (term * (int * bool)) list
+  val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
+  val read_typ: theory ->
+    (typ list * (string * sort) list) * string -> typ list * (string * sort) list
   val setup: theory -> theory
-  val print_datatypes : theory -> unit
 end;
 
 structure Datatype : DATATYPE =
@@ -56,9 +53,9 @@
 structure DatatypesData = TheoryDataFun
 (
   type T =
-    {types: datatype_info Symtab.table,
-     constrs: datatype_info Symtab.table,
-     cases: datatype_info Symtab.table};
+    {types: info Symtab.table,
+     constrs: info Symtab.table,
+     cases: info Symtab.table};
 
   val empty =
     {types = Symtab.empty, constrs = Symtab.empty, cases = Symtab.empty};
@@ -75,14 +72,10 @@
 val get_datatypes = #types o DatatypesData.get;
 val map_datatypes = DatatypesData.map;
 
-fun print_datatypes thy =
-  Pretty.writeln (Pretty.strs ("datatypes:" ::
-    map #1 (NameSpace.extern_table (Sign.type_space thy, get_datatypes thy))));
-
 
 (** theory information about datatypes **)
 
-fun put_dt_infos (dt_infos : (string * datatype_info) list) =
+fun put_dt_infos (dt_infos : (string * info) list) =
   map_datatypes (fn {types, constrs, cases} =>
     {types = fold Symtab.update dt_infos types,
      constrs = fold Symtab.default (*conservative wrt. overloaded constructors*)
@@ -207,7 +200,7 @@
   let
     val inducts = ProjectRule.projections (ProofContext.init thy) induction;
 
-    fun named_rules (name, {index, exhaustion, ...}: datatype_info) =
+    fun named_rules (name, {index, exhaustion, ...}: info) =
       [((Binding.empty, nth inducts index), [Induct.induct_type name]),
        ((Binding.empty, exhaustion), [Induct.cases_type name])];
     fun unnamed_rule i =
@@ -351,13 +344,13 @@
   simps : thm list}
 
 structure DatatypeInterpretation = InterpretationFun
-  (type T = datatype_config * string list val eq: T * T -> bool = eq_snd op =);
+  (type T = config * string list val eq: T * T -> bool = eq_snd op =);
 fun interpretation f = DatatypeInterpretation.interpretation (uncurry f);
 
 
 (******************* definitional introduction of datatypes *******************)
 
-fun add_datatype_def (config : datatype_config) new_type_names descr sorts types_syntax constr_syntax dt_info
+fun add_datatype_def (config : config) new_type_names descr sorts types_syntax constr_syntax dt_info
     case_names_induct case_names_exhausts thy =
   let
     val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
@@ -414,7 +407,7 @@
 
 (*********************** declare existing type as datatype *********************)
 
-fun prove_rep_datatype (config : datatype_config) alt_names new_type_names descr sorts induct inject half_distinct thy =
+fun prove_rep_datatype (config : config) alt_names new_type_names descr sorts induct inject half_distinct thy =
   let
     val ((_, [induct']), _) =
       Variable.importT_thms [induct] (Variable.thm_context induct);
@@ -487,7 +480,7 @@
       simps = simps}, thy11)
   end;
 
-fun gen_rep_datatype prep_term (config : datatype_config) after_qed alt_names raw_ts thy =
+fun gen_rep_datatype prep_term (config : config) after_qed alt_names raw_ts thy =
   let
     fun constr_of_term (Const (c, T)) = (c, T)
       | constr_of_term t =
@@ -553,13 +546,13 @@
   end;
 
 val rep_datatype = gen_rep_datatype Sign.cert_term;
-val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global default_datatype_config (K I);
+val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global default_config (K I);
 
 
 
 (******************************** add datatype ********************************)
 
-fun gen_add_datatype prep_typ (config : datatype_config) new_type_names dts thy =
+fun gen_add_datatype prep_typ (config : config) new_type_names dts thy =
   let
     val _ = Theory.requires thy "Datatype" "datatype definitions";
 
@@ -627,12 +620,12 @@
     val case_names_exhausts = mk_case_names_exhausts descr' (map #1 new_dts);
   in
     add_datatype_def
-      (config : datatype_config) new_type_names descr sorts types_syntax constr_syntax dt_info
+      (config : config) new_type_names descr sorts types_syntax constr_syntax dt_info
       case_names_induct case_names_exhausts thy
   end;
 
 val add_datatype = gen_add_datatype cert_typ;
-val add_datatype_cmd = gen_add_datatype read_typ default_datatype_config;
+val datatype_cmd = snd ooo gen_add_datatype read_typ default_config;
 
 
 
@@ -649,23 +642,29 @@
 
 (* outer syntax *)
 
-local structure P = OuterParse and K = OuterKeyword in
+local
 
-val 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));
+structure P = OuterParse and K = OuterKeyword
 
-fun mk_datatype args =
+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 snd o add_datatype_cmd names specs end;
+  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
-    (P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
+    (parse_datatype_decls >> (fn (names, specs) => Toplevel.theory (datatype_cmd names specs)));
 
 val _ =
   OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_goal
diff -r ec013c3ade5a -r 5fb12f859de6 src/HOL/Tools/datatype_package/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_package/datatype_abs_proofs.ML	Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_abs_proofs.ML	Sun Jun 21 19:09:31 2009 +0200
@@ -14,24 +14,22 @@
 
 signature DATATYPE_ABS_PROOFS =
 sig
-  type datatype_config = DatatypeAux.datatype_config
-  type descr = DatatypeAux.descr
-  type datatype_info = DatatypeAux.datatype_info
-  val prove_casedist_thms : datatype_config -> string list ->
+  include DATATYPE_COMMON
+  val prove_casedist_thms : config -> string list ->
     descr list -> (string * sort) list -> thm ->
     attribute list -> theory -> thm list * theory
-  val prove_primrec_thms : datatype_config -> string list ->
+  val prove_primrec_thms : config -> string list ->
     descr list -> (string * sort) list ->
-      datatype_info Symtab.table -> thm list list -> thm list list ->
+      info Symtab.table -> thm list list -> thm list list ->
         simpset -> thm -> theory -> (string list * thm list) * theory
-  val prove_case_thms : datatype_config -> string list ->
+  val prove_case_thms : config -> string list ->
     descr list -> (string * sort) list ->
       string list -> thm list -> theory -> (thm list list * string list) * theory
-  val prove_split_thms : datatype_config -> string list ->
+  val prove_split_thms : config -> string list ->
     descr list -> (string * sort) list ->
       thm list list -> thm list list -> thm list -> thm list list -> theory ->
         (thm * thm) list * theory
-  val prove_nchotomys : datatype_config -> string list -> descr list ->
+  val prove_nchotomys : config -> string list -> descr list ->
     (string * sort) list -> thm list -> theory -> thm list * theory
   val prove_weak_case_congs : string list -> descr list ->
     (string * sort) list -> theory -> thm list * theory
@@ -47,7 +45,7 @@
 
 (************************ case distinction theorems ***************************)
 
-fun prove_casedist_thms (config : datatype_config) new_type_names descr sorts induct case_names_exhausts thy =
+fun prove_casedist_thms (config : config) new_type_names descr sorts induct case_names_exhausts thy =
   let
     val _ = message config "Proving case distinction theorems ...";
 
@@ -89,8 +87,8 @@
 
 (*************************** primrec combinators ******************************)
 
-fun prove_primrec_thms (config : datatype_config) new_type_names descr sorts
-    (dt_info : datatype_info Symtab.table) constr_inject dist_rewrites dist_ss induct thy =
+fun prove_primrec_thms (config : config) new_type_names descr sorts
+    (dt_info : info Symtab.table) constr_inject dist_rewrites dist_ss induct thy =
   let
     val _ = message config "Constructing primrec combinators ...";
 
@@ -275,7 +273,7 @@
 
 (***************************** case combinators *******************************)
 
-fun prove_case_thms (config : datatype_config) new_type_names descr sorts reccomb_names primrec_thms thy =
+fun prove_case_thms (config : config) new_type_names descr sorts reccomb_names primrec_thms thy =
   let
     val _ = message config "Proving characteristic theorems for case combinators ...";
 
@@ -349,7 +347,7 @@
 
 (******************************* case splitting *******************************)
 
-fun prove_split_thms (config : datatype_config) new_type_names descr sorts constr_inject dist_rewrites
+fun prove_split_thms (config : config) new_type_names descr sorts constr_inject dist_rewrites
     casedist_thms case_thms thy =
   let
     val _ = message config "Proving equations for case splitting ...";
@@ -398,7 +396,7 @@
 
 (************************* additional theorems for TFL ************************)
 
-fun prove_nchotomys (config : datatype_config) new_type_names descr sorts casedist_thms thy =
+fun prove_nchotomys (config : config) new_type_names descr sorts casedist_thms thy =
   let
     val _ = message config "Proving additional theorems for TFL ...";
 
diff -r ec013c3ade5a -r 5fb12f859de6 src/HOL/Tools/datatype_package/datatype_aux.ML
--- a/src/HOL/Tools/datatype_package/datatype_aux.ML	Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_aux.ML	Sun Jun 21 19:09:31 2009 +0200
@@ -4,11 +4,23 @@
 Auxiliary functions for defining datatypes.
 *)
 
+signature DATATYPE_COMMON =
+sig
+  type config
+  val default_config : config
+  datatype dtyp =
+      DtTFree of string
+    | DtType of string * (dtyp list)
+    | DtRec of int;
+  type descr
+  type info
+end
+
 signature DATATYPE_AUX =
 sig
-  type datatype_config
-  val default_datatype_config : datatype_config
-  val message : datatype_config -> string -> unit
+  include DATATYPE_COMMON
+
+  val message : config -> string -> unit
   
   val add_path : bool -> string -> theory -> theory
   val parent_path : bool -> theory -> theory
@@ -33,12 +45,6 @@
   datatype simproc_dist = FewConstrs of thm list
                         | ManyConstrs of thm * simpset;
 
-  datatype dtyp =
-      DtTFree of string
-    | DtType of string * (dtyp list)
-    | DtRec of int;
-  type descr
-  type datatype_info
 
   exception Datatype
   exception Datatype_Empty of string
@@ -61,7 +67,7 @@
     -> ((string * Term.typ list) * (string * 'a list) list) list
   val check_nonempty : descr list -> unit
   val unfold_datatypes : 
-    theory -> descr -> (string * sort) list -> datatype_info Symtab.table ->
+    theory -> descr -> (string * sort) list -> info Symtab.table ->
       descr -> int -> descr list * int
 end;
 
@@ -70,10 +76,10 @@
 
 (* datatype option flags *)
 
-type datatype_config = { strict: bool, flat_names: bool, quiet: bool };
-val default_datatype_config : datatype_config =
+type config = { strict: bool, flat_names: bool, quiet: bool };
+val default_config : config =
   { strict = true, flat_names = false, quiet = false };
-fun message ({ quiet, ...} : datatype_config) s =
+fun message ({ quiet, ...} : config) s =
   if quiet then () else writeln s;
 
 fun add_path flat_names s = if flat_names then I else Sign.add_path s;
@@ -186,7 +192,7 @@
 (* index, datatype name, type arguments, constructor name, types of constructor's arguments *)
 type descr = (int * (string * dtyp list * (string * dtyp list) list)) list;
 
-type datatype_info =
+type info =
   {index : int,
    alt_names : string list option,
    descr : descr,
@@ -317,7 +323,7 @@
 (* all types of the form DtType (dt_name, [..., DtRec _, ...]) *)
 (* need to be unfolded                                         *)
 
-fun unfold_datatypes sign orig_descr sorts (dt_info : datatype_info Symtab.table) descr i =
+fun unfold_datatypes sign orig_descr sorts (dt_info : info Symtab.table) descr i =
   let
     fun typ_error T msg = error ("Non-admissible type expression\n" ^
       Syntax.string_of_typ_global sign (typ_of_dtyp (orig_descr @ descr) sorts T) ^ "\n" ^ msg);
diff -r ec013c3ade5a -r 5fb12f859de6 src/HOL/Tools/datatype_package/datatype_case.ML
--- a/src/HOL/Tools/datatype_package/datatype_case.ML	Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_case.ML	Sun Jun 21 19:09:31 2009 +0200
@@ -7,16 +7,16 @@
 
 signature DATATYPE_CASE =
 sig
-  val make_case: (string -> DatatypeAux.datatype_info option) ->
+  val make_case: (string -> DatatypeAux.info option) ->
     Proof.context -> bool -> string list -> term -> (term * term) list ->
     term * (term * (int * bool)) list
-  val dest_case: (string -> DatatypeAux.datatype_info option) -> bool ->
+  val dest_case: (string -> DatatypeAux.info option) -> bool ->
     string list -> term -> (term * (term * term) list) option
-  val strip_case: (string -> DatatypeAux.datatype_info option) -> bool ->
+  val strip_case: (string -> DatatypeAux.info option) -> bool ->
     term -> (term * (term * term) list) option
-  val case_tr: bool -> (theory -> string -> DatatypeAux.datatype_info option)
+  val case_tr: bool -> (theory -> string -> DatatypeAux.info option)
     -> Proof.context -> term list -> term
-  val case_tr': (theory -> string -> DatatypeAux.datatype_info option) ->
+  val case_tr': (theory -> string -> DatatypeAux.info option) ->
     string -> Proof.context -> term list -> term
 end;
 
@@ -31,7 +31,7 @@
  * Get information about datatypes
  *---------------------------------------------------------------------------*)
 
-fun ty_info (tab : string -> DatatypeAux.datatype_info option) s =
+fun ty_info (tab : string -> DatatypeAux.info option) s =
   case tab s of
     SOME {descr, case_name, index, sorts, ...} =>
       let
diff -r ec013c3ade5a -r 5fb12f859de6 src/HOL/Tools/datatype_package/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_package/datatype_codegen.ML	Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_codegen.ML	Sun Jun 21 19:09:31 2009 +0200
@@ -6,7 +6,7 @@
 
 signature DATATYPE_CODEGEN =
 sig
-  val find_shortest_path: DatatypeAux.descr -> int -> (string * int) option
+  val find_shortest_path: Datatype.descr -> int -> (string * int) option
   val mk_eq_eqns: theory -> string -> (thm * bool) list
   val mk_case_cert: theory -> string -> thm
   val setup: theory -> theory
@@ -17,7 +17,7 @@
 
 (** find shortest path to constructor with no recursive arguments **)
 
-fun find_nonempty (descr: DatatypeAux.descr) is i =
+fun find_nonempty (descr: Datatype.descr) is i =
   let
     val (_, _, constrs) = the (AList.lookup (op =) descr i);
     fun arg_nonempty (_, DatatypeAux.DtRec i) = if member (op =) is i
@@ -42,7 +42,7 @@
 
 (* datatype definition *)
 
-fun add_dt_defs thy defs dep module (descr: DatatypeAux.descr) sorts gr =
+fun add_dt_defs thy defs dep module (descr: Datatype.descr) sorts gr =
   let
     val descr' = List.filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr;
     val rtnames = map (#1 o snd) (List.filter (fn (_, (_, _, cs)) =>
diff -r ec013c3ade5a -r 5fb12f859de6 src/HOL/Tools/datatype_package/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_package/datatype_realizer.ML	Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_realizer.ML	Sun Jun 21 19:09:31 2009 +0200
@@ -7,7 +7,7 @@
 
 signature DATATYPE_REALIZER =
 sig
-  val add_dt_realizers: DatatypeAux.datatype_config -> string list -> theory -> theory
+  val add_dt_realizers: Datatype.config -> string list -> theory -> theory
   val setup: theory -> theory
 end;
 
@@ -38,7 +38,7 @@
 
 fun mk_realizes T = Const ("realizes", T --> HOLogic.boolT --> HOLogic.boolT);
 
-fun make_ind sorts ({descr, rec_names, rec_rewrites, induction, ...} : datatype_info) is thy =
+fun make_ind sorts ({descr, rec_names, rec_rewrites, induction, ...} : info) is thy =
   let
     val recTs = get_rec_types descr sorts;
     val pnames = if length descr = 1 then ["P"]
@@ -157,7 +157,7 @@
   in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
 
 
-fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaustion, ...} : datatype_info) thy =
+fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaustion, ...} : info) thy =
   let
     val cert = cterm_of thy;
     val rT = TFree ("'P", HOLogic.typeS);
diff -r ec013c3ade5a -r 5fb12f859de6 src/HOL/Tools/datatype_package/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML	Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML	Sun Jun 21 19:09:31 2009 +0200
@@ -11,12 +11,10 @@
 
 signature DATATYPE_REP_PROOFS =
 sig
-  type datatype_config = DatatypeAux.datatype_config
-  type descr = DatatypeAux.descr
-  type datatype_info = DatatypeAux.datatype_info
+  include DATATYPE_COMMON
   val distinctness_limit : int Config.T
   val distinctness_limit_setup : theory -> theory
-  val representation_proofs : datatype_config -> datatype_info Symtab.table ->
+  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 list list *
@@ -43,12 +41,12 @@
 val myinv_f_f = thm "myinv_f_f";
 
 
-fun exh_thm_of (dt_info : datatype_info Symtab.table) tname =
+fun exh_thm_of (dt_info : info Symtab.table) tname =
   #exhaustion (the (Symtab.lookup dt_info tname));
 
 (******************************************************************************)
 
-fun representation_proofs (config : datatype_config) (dt_info : datatype_info Symtab.table)
+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;
diff -r ec013c3ade5a -r 5fb12f859de6 src/HOL/Tools/function_package/size.ML
--- a/src/HOL/Tools/function_package/size.ML	Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOL/Tools/function_package/size.ML	Sun Jun 21 19:09:31 2009 +0200
@@ -57,7 +57,7 @@
 
 val app = curry (list_comb o swap);
 
-fun prove_size_thms (info : datatype_info) new_type_names thy =
+fun prove_size_thms (info : info) new_type_names thy =
   let
     val {descr, alt_names, sorts, rec_names, rec_rewrites, induction, ...} = info;
     val l = length new_type_names;
diff -r ec013c3ade5a -r 5fb12f859de6 src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOL/Tools/hologic.ML	Sun Jun 21 19:09:31 2009 +0200
@@ -603,8 +603,11 @@
 
 val typerepT = Type ("Typerep.typerep", []);
 
-fun mk_typerep T = Const ("Typerep.typerep_class.typerep",
-  Term.itselfT T --> typerepT) $ Logic.mk_type T;
+fun mk_typerep (Type (tyco, Ts)) = Const ("Typerep.typerep.Typerep",
+      literalT --> listT typerepT --> typerepT) $ mk_literal tyco
+        $ mk_list typerepT (map mk_typerep Ts)
+  | mk_typerep (T as TFree _) = Const ("Typerep.typerep_class.typerep",
+      Term.itselfT T --> typerepT) $ Logic.mk_type T;
 
 val termT = Type ("Code_Eval.term", []);
 
diff -r ec013c3ade5a -r 5fb12f859de6 src/HOL/Tools/old_primrec.ML
--- a/src/HOL/Tools/old_primrec.ML	Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOL/Tools/old_primrec.ML	Sun Jun 21 19:09:31 2009 +0200
@@ -221,7 +221,7 @@
 
 (* find datatypes which contain all datatypes in tnames' *)
 
-fun find_dts (dt_info : datatype_info Symtab.table) _ [] = []
+fun find_dts (dt_info : info Symtab.table) _ [] = []
   | find_dts dt_info tnames' (tname::tnames) =
       (case Symtab.lookup dt_info tname of
           NONE => primrec_err (quote tname ^ " is not a datatype")
@@ -230,7 +230,7 @@
               (tname, dt)::(find_dts dt_info tnames' tnames)
             else find_dts dt_info tnames' tnames);
 
-fun prepare_induct ({descr, induction, ...}: datatype_info) rec_eqns =
+fun prepare_induct ({descr, induction, ...}: info) rec_eqns =
   let
     fun constrs_of (_, (_, _, cs)) =
       map (fn (cname:string, (_, cargs, _, _, _)) => (cname, map fst cargs)) cs;
diff -r ec013c3ade5a -r 5fb12f859de6 src/HOL/Tools/primrec.ML
--- a/src/HOL/Tools/primrec.ML	Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOL/Tools/primrec.ML	Sun Jun 21 19:09:31 2009 +0200
@@ -203,7 +203,7 @@
 
 (* find datatypes which contain all datatypes in tnames' *)
 
-fun find_dts (dt_info : datatype_info Symtab.table) _ [] = []
+fun find_dts (dt_info : info Symtab.table) _ [] = []
   | find_dts dt_info tnames' (tname::tnames) =
       (case Symtab.lookup dt_info tname of
           NONE => primrec_error (quote tname ^ " is not a datatype")
diff -r ec013c3ade5a -r 5fb12f859de6 src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML	Sun Jun 21 19:09:31 2009 +0200
@@ -12,10 +12,10 @@
     -> seed -> (('a -> 'b) * (unit -> Term.term)) * seed
   val ensure_random_typecopy: string -> theory -> theory
   val random_aux_specification: string -> term list -> local_theory -> local_theory
-  val mk_random_aux_eqs: theory -> DatatypeAux.descr -> (string * sort) list
+  val mk_random_aux_eqs: theory -> Datatype.descr -> (string * sort) list
     -> string list -> string list * string list -> typ list * typ list
     -> string * (term list * (term * term) list)
-  val ensure_random_datatype: DatatypeAux.datatype_config -> string list -> theory -> theory
+  val ensure_random_datatype: Datatype.config -> string list -> theory -> theory
   val eval_ref: (unit -> int -> seed -> term list option * seed) option ref
   val setup: theory -> theory
 end;
diff -r ec013c3ade5a -r 5fb12f859de6 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOL/Tools/refute.ML	Sun Jun 21 19:09:31 2009 +0200
@@ -73,7 +73,7 @@
   val specialize_type : theory -> (string * Term.typ) -> Term.term -> Term.term
   val string_of_typ : Term.typ -> string
   val typ_of_dtyp :
-    DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> DatatypeAux.dtyp
+    Datatype.descr -> (Datatype.dtyp * Term.typ) list -> Datatype.dtyp
     -> Term.typ
 end;  (* signature REFUTE *)
 
@@ -411,15 +411,6 @@
 (* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL       *)
 (* ------------------------------------------------------------------------- *)
 
-(* ------------------------------------------------------------------------- *)
-(* typ_of_dtyp: converts a data type ('DatatypeAux.dtyp') into a type        *)
-(*              ('Term.typ'), given type parameters for the data type's type *)
-(*              arguments                                                    *)
-(* ------------------------------------------------------------------------- *)
-
-  (* DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list ->
-    DatatypeAux.dtyp -> Term.typ *)
-
   fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) =
     (* replace a 'DtTFree' variable by the associated type *)
     the (AList.lookup (op =) typ_assoc (DatatypeAux.DtTFree a))
@@ -1660,10 +1651,6 @@
 (*               their arguments) of the size of the argument types          *)
 (* ------------------------------------------------------------------------- *)
 
-  (* theory -> (Term.typ * int) list -> DatatypeAux.descr ->
-    (DatatypeAux.dtyp * Term.typ) list ->
-    (string * DatatypeAux.dtyp list) list -> int *)
-
   fun size_of_dtyp thy typ_sizes descr typ_assoc constructors =
     sum (map (fn (_, dtyps) =>
       product (map (size_of_type thy (typ_sizes, []) o
@@ -2144,7 +2131,6 @@
               (* decrement depth for the IDT 'T' *)
               val typs' = (case AList.lookup (op =) typs T of NONE => typs
                 | SOME n => AList.update (op =) (T, n-1) typs)
-              (* Term.term list -> DatatypeAux.dtyp list -> Term.term list *)
               fun constructor_terms terms [] = terms
                 | constructor_terms terms (d::ds) =
                 let
@@ -2241,7 +2227,6 @@
                     else ()
                   (* returns an interpretation where everything is mapped to *)
                   (* an "undefined" element of the datatype                  *)
-                  (* DatatypeAux.dtyp list -> interpretation *)
                   fun make_undef [] =
                     Leaf (replicate total False)
                     | make_undef (d::ds) =
@@ -2253,7 +2238,6 @@
                       Node (replicate size (make_undef ds))
                     end
                   (* returns the interpretation for a constructor *)
-                  (* int * DatatypeAux.dtyp list -> int * interpretation *)
                   fun make_constr (offset, []) =
                     if offset<total then
                       (offset+1, Leaf ((replicate offset False) @ True ::
@@ -2421,9 +2405,6 @@
                   (* mutually recursive types must have the same type   *)
                   (* parameters, unless the mutual recursion comes from *)
                   (* indirect recursion                                 *)
-                  (* (DatatypeAux.dtyp * Term.typ) list ->
-                    (DatatypeAux.dtyp * Term.typ) list ->
-                    (DatatypeAux.dtyp * Term.typ) list *)
                   fun rec_typ_assoc acc [] =
                     acc
                     | rec_typ_assoc acc ((d, T)::xs) =
@@ -2458,7 +2439,6 @@
                       else
                         raise REFUTE ("IDT_recursion_interpreter",
                           "different type associations for the same dtyp"))
-                  (* (DatatypeAux.dtyp * Term.typ) list *)
                   val typ_assoc = filter
                     (fn (DatatypeAux.DtTFree _, _) => true | (_, _) => false)
                     (rec_typ_assoc []
@@ -2613,7 +2593,6 @@
                         val rec_dtyps_args  = List.filter
                           (DatatypeAux.is_rec_type o fst) (dtyps ~~ args)
                         (* map those indices to interpretations *)
-                        (* (DatatypeAux.dtyp * interpretation) list *)
                         val rec_dtyps_intrs = map (fn (dtyp, arg) =>
                           let
                             val dT     = typ_of_dtyp descr typ_assoc dtyp
@@ -2625,8 +2604,6 @@
                         (* takes the dtyp and interpretation of an element, *)
                         (* and computes the interpretation for the          *)
                         (* corresponding recursive argument                 *)
-                        (* DatatypeAux.dtyp -> interpretation ->
-                          interpretation *)
                         fun rec_intr (DatatypeAux.DtRec i) (Leaf xs) =
                           (* recursive argument is "rec_i params elem" *)
                           compute_array_entry i (find_index_eq True xs)
@@ -3252,8 +3229,6 @@
             (* constructor generates the datatype's element that is given by *)
             (* 'element', returns the constructor (as a term) as well as the *)
             (* indices of the arguments                                      *)
-            (* string * DatatypeAux.dtyp list ->
-              (Term.term * int list) option *)
             fun get_constr_args (cname, cargs) =
               let
                 val cTerm      = Const (cname,
@@ -3281,7 +3256,6 @@
               in
                 Option.map (fn args => (cTerm, cargs, args)) (get_args iC)
               end
-            (* Term.term * DatatypeAux.dtyp list * int list *)
             val (cTerm, cargs, args) =
               (* we could speed things up by computing the correct          *)
               (* constructor directly (rather than testing all              *)
diff -r ec013c3ade5a -r 5fb12f859de6 src/HOL/Tools/typecopy.ML
--- a/src/HOL/Tools/typecopy.ML	Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOL/Tools/typecopy.ML	Sun Jun 21 19:09:31 2009 +0200
@@ -6,21 +6,13 @@
 
 signature TYPECOPY =
 sig
-  type info = {
-    vs: (string * sort) list,
-    constr: string,
-    typ: typ,
-    inject: thm,
-    proj: string * typ,
-    proj_def: thm
-  }
+  type info = { vs: (string * sort) list, constr: string, typ: typ,
+    inject: thm, proj: string * typ, proj_def: thm }
   val typecopy: binding * string list -> typ -> (binding * binding) option
     -> theory -> (string * info) * theory
-  val get_typecopies: theory -> string list
   val get_info: theory -> string -> info option
   val interpretation: (string -> theory -> theory) -> theory -> theory
   val add_default_code: string -> theory -> theory
-  val print_typecopies: theory -> unit
   val setup: theory -> theory
 end;
 
@@ -47,22 +39,6 @@
   fun merge _ = Symtab.merge (K true);
 );
 
-fun print_typecopies thy =
-  let
-    val tab = TypecopyData.get thy;
-    fun mk (tyco, { vs, constr, typ, proj = (proj, _), ... } : info) =
-      (Pretty.block o Pretty.breaks) [
-        Syntax.pretty_typ_global thy (Type (tyco, map TFree vs)),
-        Pretty.str "=",
-        (Pretty.str o Sign.extern_const thy) constr,
-        Syntax.pretty_typ_global thy typ,
-        Pretty.block [Pretty.str "(", (Pretty.str o Sign.extern_const thy) proj, Pretty.str  ")"]];
-    in
-      (Pretty.writeln o Pretty.block o Pretty.fbreaks)
-        (Pretty.str "type copies:" :: map mk (Symtab.dest tab))
-    end;
-
-val get_typecopies = Symtab.keys o TypecopyData.get;
 val get_info = Symtab.lookup o TypecopyData.get;
 
 
@@ -72,7 +48,7 @@
 val interpretation = TypecopyInterpretation.interpretation;
 
 
-(* declaring typecopies *)
+(* introducing typecopies *)
 
 fun typecopy (raw_tyco, raw_vs) raw_ty constr_proj thy =
   let
diff -r ec013c3ade5a -r 5fb12f859de6 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOL/Tools/typedef.ML	Sun Jun 21 19:09:31 2009 +0200
@@ -12,13 +12,13 @@
     type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
     Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
     Rep_induct: thm, Abs_induct: thm}
-  val get_info: theory -> string -> info option
   val add_typedef: bool -> binding option -> binding * string list * mixfix ->
     term -> (binding * binding) option -> tactic -> theory -> (string * info) * theory
   val typedef: (bool * binding) * (binding * string list * mixfix) * term
     * (binding * binding) option -> theory -> Proof.state
   val typedef_cmd: (bool * binding) * (binding * string list * mixfix) * string
     * (binding * binding) option -> theory -> Proof.state
+  val get_info: theory -> string -> info option
   val interpretation: (string -> theory -> theory) -> theory -> theory
   val setup: theory -> theory
 end;
diff -r ec013c3ade5a -r 5fb12f859de6 src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOLCF/Fixrec.thy	Sun Jun 21 19:09:31 2009 +0200
@@ -6,7 +6,7 @@
 
 theory Fixrec
 imports Sprod Ssum Up One Tr Fix
-uses ("Tools/fixrec_package.ML")
+uses ("Tools/fixrec.ML")
 begin
 
 subsection {* Maybe monad type *}
@@ -599,12 +599,12 @@
 
 subsection {* Initializing the fixrec package *}
 
-use "Tools/fixrec_package.ML"
+use "Tools/fixrec.ML"
 
-setup {* FixrecPackage.setup *}
+setup {* Fixrec.setup *}
 
 setup {*
-  FixrecPackage.add_matchers
+  Fixrec.add_matchers
     [ (@{const_name up}, @{const_name match_up}),
       (@{const_name sinl}, @{const_name match_sinl}),
       (@{const_name sinr}, @{const_name match_sinr}),
diff -r ec013c3ade5a -r 5fb12f859de6 src/HOLCF/IOA/meta_theory/Abstraction.thy
--- a/src/HOLCF/IOA/meta_theory/Abstraction.thy	Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy	Sun Jun 21 19:09:31 2009 +0200
@@ -6,7 +6,7 @@
 
 theory Abstraction
 imports LiveIOA
-uses ("ioa_package.ML")
+uses ("ioa.ML")
 begin
 
 defaultsort type
@@ -613,6 +613,6 @@
 
 method_setup abstraction = {* Scan.succeed (SIMPLE_METHOD' o abstraction_tac) *} ""
 
-use "ioa_package.ML"
+use "ioa.ML"
 
 end
diff -r ec013c3ade5a -r 5fb12f859de6 src/HOLCF/IOA/meta_theory/ioa_package.ML
--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Sun Jun 21 19:09:31 2009 +0200
@@ -1,9 +1,8 @@
-(*  Title:      HOLCF/IOA/meta_theory/ioa_package.ML
-    ID:         $Id$
+(*  Title:      HOLCF/IOA/meta_theory/ioa.ML
     Author:     Tobias Hamberger, TU Muenchen
 *)
 
-signature IOA_PACKAGE =
+signature IOA =
 sig
   val add_ioa: string -> string
     -> (string) list -> (string) list -> (string) list
@@ -16,7 +15,7 @@
   val add_rename : string -> string -> string -> theory -> theory
 end;
 
-structure IoaPackage: IOA_PACKAGE =
+structure Ioa: IOA =
 struct
 
 val string_of_typ = PrintMode.setmp [] o Syntax.string_of_typ_global;
diff -r ec013c3ade5a -r 5fb12f859de6 src/HOLCF/IsaMakefile
--- a/src/HOLCF/IsaMakefile	Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOLCF/IsaMakefile	Sun Jun 21 19:09:31 2009 +0200
@@ -67,8 +67,8 @@
   Tools/domain/domain_library.ML \
   Tools/domain/domain_syntax.ML \
   Tools/domain/domain_theorems.ML \
-  Tools/fixrec_package.ML \
-  Tools/pcpodef_package.ML \
+  Tools/fixrec.ML \
+  Tools/pcpodef.ML \
   holcf_logic.ML \
   document/root.tex
 	@$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/HOL HOLCF
@@ -127,7 +127,7 @@
   IOA/meta_theory/TL.thy IOA/meta_theory/TLS.thy		       \
   IOA/meta_theory/LiveIOA.thy IOA/meta_theory/Pred.thy		       \
   IOA/meta_theory/Abstraction.thy IOA/meta_theory/Simulations.thy      \
-  IOA/meta_theory/SimCorrectness.thy IOA/meta_theory/ioa_package.ML
+  IOA/meta_theory/SimCorrectness.thy IOA/meta_theory/ioa.ML
 	@cd IOA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOLCF IOA
 
 
diff -r ec013c3ade5a -r 5fb12f859de6 src/HOLCF/Pcpodef.thy
--- a/src/HOLCF/Pcpodef.thy	Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOLCF/Pcpodef.thy	Sun Jun 21 19:09:31 2009 +0200
@@ -6,7 +6,7 @@
 
 theory Pcpodef
 imports Adm
-uses ("Tools/pcpodef_package.ML")
+uses ("Tools/pcpodef.ML")
 begin
 
 subsection {* Proving a subtype is a partial order *}
@@ -303,6 +303,6 @@
 
 subsection {* HOLCF type definition package *}
 
-use "Tools/pcpodef_package.ML"
+use "Tools/pcpodef.ML"
 
 end
diff -r ec013c3ade5a -r 5fb12f859de6 src/HOLCF/Tools/domain/domain_axioms.ML
--- a/src/HOLCF/Tools/domain/domain_axioms.ML	Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_axioms.ML	Sun Jun 21 19:09:31 2009 +0200
@@ -6,7 +6,7 @@
 
 signature DOMAIN_AXIOMS =
 sig
-  val copy_of_dtyp : (int -> term) -> DatatypeAux.dtyp -> term
+  val copy_of_dtyp : (int -> term) -> Datatype.dtyp -> term
 
   val calc_axioms :
       string -> Domain_Library.eq list -> int -> Domain_Library.eq ->
@@ -171,7 +171,7 @@
       val mat_names = map mat_name con_names;
       fun qualify n = Sign.full_name thy (Binding.name n);
       val ms = map qualify con_names ~~ map qualify mat_names;
-    in FixrecPackage.add_matchers ms thy end;
+    in Fixrec.add_matchers ms thy end;
 
 fun add_axioms comp_dnam (eqs : eq list) thy' =
     let
diff -r ec013c3ade5a -r 5fb12f859de6 src/HOLCF/Tools/domain/domain_library.ML
--- a/src/HOLCF/Tools/domain/domain_library.ML	Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_library.ML	Sun Jun 21 19:09:31 2009 +0200
@@ -135,10 +135,10 @@
       eqtype arg;
   type cons = string * arg list;
   type eq = (string * typ list) * cons list;
-  val mk_arg : (bool * DatatypeAux.dtyp) * string option * string -> arg;
+  val mk_arg : (bool * Datatype.dtyp) * string option * string -> arg;
   val is_lazy : arg -> bool;
   val rec_of : arg -> int;
-  val dtyp_of : arg -> DatatypeAux.dtyp;
+  val dtyp_of : arg -> Datatype.dtyp;
   val sel_of : arg -> string option;
   val vname : arg -> string;
   val upd_vname : (string -> string) -> arg -> arg;
@@ -154,7 +154,7 @@
   val idx_name : 'a list -> string -> int -> string;
   val app_rec_arg : (int -> term) -> arg -> term;
   val con_app : string -> arg list -> term;
-  val dtyp_of_eq : eq -> DatatypeAux.dtyp;
+  val dtyp_of_eq : eq -> Datatype.dtyp;
 
 
   (* Name mangling *)
@@ -215,7 +215,7 @@
 (* ----- constructor list handling ----- *)
 
 type arg =
-     (bool * DatatypeAux.dtyp) *   (*  (lazy, recursive element) *)
+     (bool * Datatype.dtyp) *   (*  (lazy, recursive element) *)
      string option *               (*   selector name    *)
      string;                       (*   argument name    *)
 
diff -r ec013c3ade5a -r 5fb12f859de6 src/HOLCF/Tools/fixrec_package.ML
--- a/src/HOLCF/Tools/fixrec_package.ML	Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOLCF/Tools/fixrec_package.ML	Sun Jun 21 19:09:31 2009 +0200
@@ -1,10 +1,10 @@
-(*  Title:      HOLCF/Tools/fixrec_package.ML
+(*  Title:      HOLCF/Tools/fixrec.ML
     Author:     Amber Telfer and Brian Huffman
 
 Recursive function definition package for HOLCF.
 *)
 
-signature FIXREC_PACKAGE =
+signature FIXREC =
 sig
   val add_fixrec: bool -> (binding * typ option * mixfix) list
     -> (Attrib.binding * term) list -> local_theory -> local_theory
@@ -16,7 +16,7 @@
   val setup: theory -> theory
 end;
 
-structure FixrecPackage :> FIXREC_PACKAGE =
+structure Fixrec :> FIXREC =
 struct
 
 val def_cont_fix_eq = @{thm def_cont_fix_eq};
@@ -327,7 +327,7 @@
 (*************************************************************************)
 
 local
-(* code adapted from HOL/Tools/primrec_package.ML *)
+(* code adapted from HOL/Tools/primrec.ML *)
 
 fun gen_fixrec
   (set_group : bool)
diff -r ec013c3ade5a -r 5fb12f859de6 src/HOLCF/Tools/pcpodef_package.ML
--- a/src/HOLCF/Tools/pcpodef_package.ML	Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOLCF/Tools/pcpodef_package.ML	Sun Jun 21 19:09:31 2009 +0200
@@ -1,11 +1,11 @@
-(*  Title:      HOLCF/Tools/pcpodef_package.ML
+(*  Title:      HOLCF/Tools/pcpodef.ML
     Author:     Brian Huffman
 
 Primitive domain definitions for HOLCF, similar to Gordon/HOL-style
-typedef (see also ~~/src/HOL/Tools/typedef_package.ML).
+typedef (see also ~~/src/HOL/Tools/typedef.ML).
 *)
 
-signature PCPODEF_PACKAGE =
+signature PCPODEF =
 sig
   val pcpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
     * (binding * binding) option -> theory -> Proof.state
@@ -17,7 +17,7 @@
     * (binding * binding) option -> theory -> Proof.state
 end;
 
-structure PcpodefPackage :> PCPODEF_PACKAGE =
+structure Pcpodef :> PCPODEF =
 struct
 
 (** type definitions **)