src/HOLCF/domain/theorems.ML
changeset 4008 2444085532c6
parent 3323 194ae2e0c193
child 4030 ca44afcc259c
     1.1 --- a/src/HOLCF/domain/theorems.ML	Mon Oct 27 10:46:36 1997 +0100
     1.2 +++ b/src/HOLCF/domain/theorems.ML	Mon Oct 27 11:34:33 1997 +0100
     1.3 @@ -62,7 +62,7 @@
     1.4  fun theorems thy (((dname,_),cons) : eq, eqs :eq list) =
     1.5  let
     1.6  
     1.7 -val dummy = writeln ("Proving isomorphism properties of domain "^dname^"...");
     1.8 +val dummy = writeln ("Proving isomorphism   properties of domain "^dname^"...");
     1.9  val pg = pg' thy;
    1.10  (*
    1.11  infixr 0 y;
    1.12 @@ -328,15 +328,16 @@
    1.13  end; (* let *)
    1.14  
    1.15  
    1.16 -fun comp_theorems thy (comp_dname, eqs: eq list, casess, con_rews, copy_rews) =
    1.17 +fun comp_theorems thy (comp_dnam, eqs: eq list, casess, con_rews, copy_rews) =
    1.18  let
    1.19  
    1.20 +val dnames = map (fst o fst) eqs;
    1.21 +val conss  = map  snd        eqs;
    1.22 +val comp_dname = Sign.full_name (sign_of thy) comp_dnam;
    1.23 +
    1.24  val dummy = writeln("Proving induction properties of domain "^comp_dname^"...");
    1.25  val pg = pg' thy;
    1.26  
    1.27 -val dnames = map (fst o fst) eqs;
    1.28 -val conss  = map  snd        eqs;
    1.29 -
    1.30  (* ----- getting the composite axiom and definitions ------------------------ *)
    1.31  
    1.32  local val ga = get_axiom thy in