# HG changeset patch
# User haftmann
# Date 1245566338 -7200
# Node ID 7b9b9ba532caad091254d7dd19cd5227e8897c93
# Parent  b3f63611784ee9fc5c4e5ab812b146b6fd9783cc
discontinued ancient tradition to suffix certain ML module names with "_package"

diff -r b3f63611784e -r 7b9b9ba532ca src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Sun Jun 21 08:38:58 2009 +0200
+++ b/src/HOLCF/Fixrec.thy	Sun Jun 21 08:38:58 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 b3f63611784e -r 7b9b9ba532ca src/HOLCF/IOA/meta_theory/Abstraction.thy
--- a/src/HOLCF/IOA/meta_theory/Abstraction.thy	Sun Jun 21 08:38:58 2009 +0200
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy	Sun Jun 21 08:38:58 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 b3f63611784e -r 7b9b9ba532ca src/HOLCF/IOA/meta_theory/ioa_package.ML
--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Sun Jun 21 08:38:58 2009 +0200
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Sun Jun 21 08:38:58 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 b3f63611784e -r 7b9b9ba532ca src/HOLCF/IsaMakefile
--- a/src/HOLCF/IsaMakefile	Sun Jun 21 08:38:58 2009 +0200
+++ b/src/HOLCF/IsaMakefile	Sun Jun 21 08:38:58 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 b3f63611784e -r 7b9b9ba532ca src/HOLCF/Pcpodef.thy
--- a/src/HOLCF/Pcpodef.thy	Sun Jun 21 08:38:58 2009 +0200
+++ b/src/HOLCF/Pcpodef.thy	Sun Jun 21 08:38:58 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 b3f63611784e -r 7b9b9ba532ca src/HOLCF/Tools/domain/domain_axioms.ML
--- a/src/HOLCF/Tools/domain/domain_axioms.ML	Sun Jun 21 08:38:58 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_axioms.ML	Sun Jun 21 08:38:58 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 b3f63611784e -r 7b9b9ba532ca src/HOLCF/Tools/domain/domain_library.ML
--- a/src/HOLCF/Tools/domain/domain_library.ML	Sun Jun 21 08:38:58 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_library.ML	Sun Jun 21 08:38:58 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 b3f63611784e -r 7b9b9ba532ca src/HOLCF/Tools/fixrec_package.ML
--- a/src/HOLCF/Tools/fixrec_package.ML	Sun Jun 21 08:38:58 2009 +0200
+++ b/src/HOLCF/Tools/fixrec_package.ML	Sun Jun 21 08:38:58 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 b3f63611784e -r 7b9b9ba532ca src/HOLCF/Tools/pcpodef_package.ML
--- a/src/HOLCF/Tools/pcpodef_package.ML	Sun Jun 21 08:38:58 2009 +0200
+++ b/src/HOLCF/Tools/pcpodef_package.ML	Sun Jun 21 08:38:58 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 **)