src/HOLCF/domain/theorems.ML
changeset 16486 1a12cdb6ee6b
parent 16462 8ebc8f530ab4
child 16778 2162c0de4673
     1.1 --- a/src/HOLCF/domain/theorems.ML	Mon Jun 20 22:13:58 2005 +0200
     1.2 +++ b/src/HOLCF/domain/theorems.ML	Mon Jun 20 22:13:59 2005 +0200
     1.3 @@ -63,7 +63,7 @@
     1.4  
     1.5  (* ----- getting the axioms and definitions --------------------------------- *)
     1.6  
     1.7 -local fun ga s dn = get_thm thy (dn ^ "." ^ s, NONE) in
     1.8 +local fun ga s dn = get_thm thy (Name (dn ^ "." ^ s)) in
     1.9  val ax_abs_iso    = ga "abs_iso"  dname;
    1.10  val ax_rep_iso    = ga "rep_iso"  dname;
    1.11  val ax_when_def   = ga "when_def" dname;
    1.12 @@ -352,7 +352,7 @@
    1.13  
    1.14  (* ----- getting the composite axiom and definitions ------------------------ *)
    1.15  
    1.16 -local fun ga s dn = get_thm thy (dn ^ "." ^ s, NONE) in
    1.17 +local fun ga s dn = get_thm thy (Name (dn ^ "." ^ s)) in
    1.18  val axs_reach      = map (ga "reach"     ) dnames;
    1.19  val axs_take_def   = map (ga "take_def"  ) dnames;
    1.20  val axs_finite_def = map (ga "finite_def") dnames;
    1.21 @@ -360,8 +360,8 @@
    1.22  val ax_bisim_def   =      ga "bisim_def" comp_dnam;
    1.23  end; (* local *)
    1.24  
    1.25 -local fun gt  s dn = get_thm  thy (dn ^ "." ^ s, NONE);
    1.26 -      fun gts s dn = get_thms thy (dn ^ "." ^ s, NONE) in
    1.27 +local fun gt  s dn = get_thm  thy (Name (dn ^ "." ^ s));
    1.28 +      fun gts s dn = get_thms thy (Name (dn ^ "." ^ s)) in
    1.29  val cases     =       map (gt  "casedist" ) dnames;
    1.30  val con_rews  = List.concat (map (gts "con_rews" ) dnames);
    1.31  val copy_rews = List.concat (map (gts "copy_rews") dnames);