Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/Tools/domain/domain_axioms.ML
changeset 31738 7b9b9ba532ca
parent 31288 67dff9c5b2bd 
--- 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
isabelle