--- a/src/HOLCF/domain/theorems.ML Mon Jun 20 22:13:58 2005 +0200
+++ b/src/HOLCF/domain/theorems.ML Mon Jun 20 22:13:59 2005 +0200
@@ -63,7 +63,7 @@
(* ----- getting the axioms and definitions --------------------------------- *)
-local fun ga s dn = get_thm thy (dn ^ "." ^ s, NONE) in
+local fun ga s dn = get_thm thy (Name (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;
@@ -352,7 +352,7 @@
(* ----- getting the composite axiom and definitions ------------------------ *)
-local fun ga s dn = get_thm thy (dn ^ "." ^ s, NONE) in
+local fun ga s dn = get_thm thy (Name (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;
@@ -360,8 +360,8 @@
val ax_bisim_def = ga "bisim_def" comp_dnam;
end; (* local *)
-local fun gt s dn = get_thm thy (dn ^ "." ^ s, NONE);
- fun gts s dn = get_thms thy (dn ^ "." ^ s, NONE) in
+local fun gt s dn = get_thm thy (Name (dn ^ "." ^ s));
+ fun gts s dn = get_thms thy (Name (dn ^ "." ^ s)) in
val cases = map (gt "casedist" ) dnames;
val con_rews = List.concat (map (gts "con_rews" ) dnames);
val copy_rews = List.concat (map (gts "copy_rews") dnames);