# HG changeset patch
# User huffman
# Date 1267569676 28800
# Node ID 0e2ef13796a475188f64a6072c9f8166c9edf7a9
# Parent  59550ec4921d21f65add0ec449904596c1cd5eb2
add_axioms no longer needs a definitional mode

diff -r 59550ec4921d -r 0e2ef13796a4 src/HOLCF/Tools/Domain/domain_axioms.ML
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Tue Mar 02 14:35:09 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Tue Mar 02 14:41:16 2010 -0800
@@ -10,12 +10,10 @@
       string Symtab.table -> (int -> term) -> Datatype.dtyp -> term
 
   val calc_axioms :
-      bool ->
       Domain_Library.eq list -> int -> Domain_Library.eq ->
       string * (string * term) list
 
   val add_axioms :
-      bool ->
       ((string * typ list) *
        (binding * (bool * binding option * typ) list * mixfix) list) list ->
       Domain_Library.eq list -> theory -> theory
@@ -49,15 +47,11 @@
     | NONE => (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID);
 
 fun calc_axioms
-    (definitional : bool)
     (eqs : eq list)
     (n : int)
     (eqn as ((dname,_),cons) : eq)
     : string * (string * term) list =
   let
-
-(* ----- axioms and definitions concerning the isomorphism ------------------ *)
-
     val dc_abs = %%:(dname^"_abs");
     val dc_rep = %%:(dname^"_rep");
     val x_name'= "x";
@@ -66,10 +60,9 @@
 
     val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name'));
     val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name'));
-
   in
-    (dnam, if definitional then [] else [abs_iso_ax, rep_iso_ax])
-  end; (* let (calc_axioms) *)
+    (dnam, [abs_iso_ax, rep_iso_ax])
+  end;
 
 
 (* legacy type inference *)
@@ -85,7 +78,7 @@
 fun add_axioms_i x = snd o PureThy.add_axioms (map (Thm.no_attributes o apfst Binding.name) x);
 fun add_axioms_infer axms thy = add_axioms_i (infer_props thy axms) thy;
 
-fun add_axioms definitional eqs' (eqs : eq list) thy' =
+fun add_axioms eqs' (eqs : eq list) thy' =
   let
     val dnames = map (fst o fst) eqs;
     val x_name = idx_name dnames "x"; 
@@ -95,7 +88,7 @@
           #> add_axioms_infer axs
           #> Sign.parent_path;
 
-    val axs = mapn (calc_axioms definitional eqs) 0 eqs;
+    val axs = mapn (calc_axioms eqs) 0 eqs;
     val thy = thy' |> fold add_one axs;
 
     fun get_iso_info ((dname, tyvars), cons') =
@@ -121,10 +114,9 @@
         }
       end;
     val dom_binds = map (Binding.name o Long_Name.base_name) dnames;
-    val thy =
-        if definitional then thy
-        else snd (Domain_Take_Proofs.define_take_functions
-                    (dom_binds ~~ map get_iso_info eqs') thy);
+    val (take_info, thy) =
+        Domain_Take_Proofs.define_take_functions
+          (dom_binds ~~ map get_iso_info eqs') thy;
 
     (* declare lub_take axioms *)
     local
@@ -141,9 +133,7 @@
           add_one (dnam, [("lub_take", ax)])
         end
     in
-      val thy =
-          if definitional then thy
-          else fold ax_lub_take dnames thy
+      val thy = fold ax_lub_take dnames thy
     end;
   in
     thy
diff -r 59550ec4921d -r 0e2ef13796a4 src/HOLCF/Tools/Domain/domain_extender.ML
--- a/src/HOLCF/Tools/Domain/domain_extender.ML	Tue Mar 02 14:35:09 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Tue Mar 02 14:41:16 2010 -0800
@@ -164,7 +164,7 @@
         ) : cons;
     val eqs : eq list =
         map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
-    val thy = thy |> Domain_Axioms.add_axioms false eqs' eqs;
+    val thy = Domain_Axioms.add_axioms eqs' eqs thy;
     val ((rewss, take_rews), theorems_thy) =
         thy
           |> fold_map (fn (eq, (x,cs)) =>
@@ -237,7 +237,6 @@
         ) : cons;
     val eqs : eq list =
         map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
-    val thy = thy |> Domain_Axioms.add_axioms true eqs' eqs;
     val ((rewss, take_rews), theorems_thy) =
         thy
           |> fold_map (fn (eq, (x,cs)) =>