src/HOLCF/Tools/domain/domain_theorems.ML

 val pg = pg' thy;
 
 (* ----- getting the axioms and definitions --------------------------------- *)
 
 local
-  fun ga s dn = PureThy.get_thm thy (Facts.Named (dn ^ "." ^ s, NONE));
+  fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s);
 in
   val ax_abs_iso  = ga "abs_iso"  dname;
   val ax_rep_iso  = ga "rep_iso"  dname;
   val ax_when_def = ga "when_def" dname;
   fun get_def mk_name (con,_) = ga (mk_name con^"_def") dname;

 val pg = pg' thy;
 
 (* ----- getting the composite axiom and definitions ------------------------ *)
 
 local
-  fun ga s dn = PureThy.get_thm thy (Facts.Named (dn ^ "." ^ s, NONE));
+  fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s);
 in
   val axs_reach      = map (ga "reach"     ) dnames;
   val axs_take_def   = map (ga "take_def"  ) dnames;
   val axs_finite_def = map (ga "finite_def") dnames;
   val ax_copy2_def   =      ga "copy_def"  comp_dnam;
   val ax_bisim_def   =      ga "bisim_def" comp_dnam;
 end;
 
 local
-  fun gt  s dn = PureThy.get_thm  thy (Facts.Named (dn ^ "." ^ s, NONE));
-  fun gts s dn = PureThy.get_thms thy (Facts.Named (dn ^ "." ^ s, NONE));
+  fun gt  s dn = PureThy.get_thm  thy (dn ^ "." ^ s);
+  fun gts s dn = PureThy.get_thms thy (dn ^ "." ^ s);
 in
   val cases = map (gt  "casedist" ) dnames;
   val con_rews  = maps (gts "con_rews" ) dnames;
   val copy_rews = maps (gts "copy_rews") dnames;
 end;