src/HOLCF/Tools/domain/domain_theorems.ML

 let
 val global_ctxt = ProofContext.init thy;
 
 val dnames = map (fst o fst) eqs;
 val conss  = map  snd        eqs;
-val comp_dname = Sign.full_name thy comp_dnam;
+val comp_dname = Sign.full_bname thy comp_dnam;
 
 val d = writeln("Proving induction properties of domain "^comp_dname^" ...");
 val pg = pg' thy;
 
 (* ----- getting the composite axiom and definitions ------------------------ *)