src/HOLCF/domain/theorems.ML
changeset 7906 0576dad973b1
parent 6092 d9db67970c73
child 8149 941afb897532
     1.1 --- a/src/HOLCF/domain/theorems.ML	Thu Oct 21 18:45:55 1999 +0200
     1.2 +++ b/src/HOLCF/domain/theorems.ML	Thu Oct 21 18:46:33 1999 +0200
     1.3 @@ -75,7 +75,7 @@
     1.4  
     1.5  (* ----- getting the axioms and definitions --------------------------------- *)
     1.6  
     1.7 -local fun ga s dn = get_axiom thy (dn^"."^s) in
     1.8 +local fun ga s dn = get_thm thy (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 @@ -350,7 +350,7 @@
    1.13  
    1.14  (* ----- getting the composite axiom and definitions ------------------------ *)
    1.15  
    1.16 -local fun ga s dn = get_axiom thy (dn^"."^s) in
    1.17 +local fun ga s dn = get_thm thy (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;