src/HOLCF/domain/theorems.ML

 
 
 fun theorems thy (((dname,_),cons) : eq, eqs :eq list) =
 let
 
-val dummy = writeln ("Proving isomorphism properties of domain "^dname^"...");
+val dummy = writeln ("Proving isomorphism   properties of domain "^dname^"...");
 val pg = pg' thy;
 (*
 infixr 0 y;
 val b = 0;
 fun _ y t = by t;

         con_rews, sel_rews, dis_rews, dists_le, dists_eq, inverts, injects,
         copy_rews)
 end; (* let *)
 
 
-fun comp_theorems thy (comp_dname, eqs: eq list, casess, con_rews, copy_rews) =
+fun comp_theorems thy (comp_dnam, eqs: eq list, casess, con_rews, copy_rews) =
 let
+
+val dnames = map (fst o fst) eqs;
+val conss  = map  snd        eqs;
+val comp_dname = Sign.full_name (sign_of thy) comp_dnam;
 
 val dummy = writeln("Proving induction properties of domain "^comp_dname^"...");
 val pg = pg' thy;
-
-val dnames = map (fst o fst) eqs;
-val conss  = map  snd        eqs;
 
 (* ----- getting the composite axiom and definitions ------------------------ *)
 
 local val ga = get_axiom thy in
 val axs_reach      = map (fn dn => ga (dn ^  "_reach"   )) dnames;