--- a/src/HOLCF/Tools/Domain/domain_axioms.ML Tue Mar 02 09:54:50 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Tue Mar 02 13:01:22 2010 -0800
@@ -10,7 +10,7 @@
string Symtab.table -> (int -> term) -> Datatype.dtyp -> term
val calc_axioms :
- bool -> string Symtab.table ->
+ bool ->
Domain_Library.eq list -> int -> Domain_Library.eq ->
string * (string * term) list * (string * term) list
@@ -50,7 +50,6 @@
fun calc_axioms
(definitional : bool)
- (map_tab : string Symtab.table)
(eqs : eq list)
(n : int)
(eqn as ((dname,_),cons) : eq)
@@ -108,8 +107,7 @@
#> add_axioms_infer axs
#> Sign.parent_path;
- val map_tab = Domain_Isomorphism.get_map_tab thy';
- val axs = mapn (calc_axioms definitional map_tab eqs) 0 eqs;
+ val axs = mapn (calc_axioms definitional eqs) 0 eqs;
val thy = thy' |> fold add_one axs;
fun get_iso_info ((dname, tyvars), cons') =