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
```