# HG changeset patch
# User huffman
# Date 1268543240 28800
# Node ID 8a314dd86714bd213d96d9e87b517798e4db6bbf
# Parent  b7738ab762b165fd89c5c3bbfa1ef380e55bba76
add case name 'adm' for infinite induction rules

diff -r b7738ab762b1 -r 8a314dd86714 src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat Mar 13 20:15:25 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat Mar 13 21:07:20 2010 -0800
@@ -392,12 +392,16 @@
 
 val case_ns =
   let
+    val adms =
+        if is_finite then [] else
+        if length dnames = 1 then ["adm"] else
+        map (fn s => "adm_" ^ Long_Name.base_name s) dnames;
     val bottoms =
         if length dnames = 1 then ["bottom"] else
         map (fn s => "bottom_" ^ Long_Name.base_name s) dnames;
     fun one_eq bot (_,cons) =
           bot :: map (fn (c,_) => Long_Name.base_name c) cons;
-  in flat (map2 one_eq bottoms eqs) end;
+  in adms @ flat (map2 one_eq bottoms eqs) end;
 
 val inducts = Project_Rule.projections (ProofContext.init thy) ind;
 fun ind_rule (dname, rule) =