1.1 --- a/TFL/tfl.sml	Thu Oct 21 18:45:55 1999 +0200
     1.2 +++ b/TFL/tfl.sml	Thu Oct 21 18:46:33 1999 +0200
     1.3 @@ -538,7 +538,7 @@
     1.4         thy
     1.5         |> PureThy.add_defs_i 
     1.6              [Thm.no_attributes (fid ^ "_def", defn)]
     1.7 -     val def = freezeT (get_axiom theory (fid ^ "_def"))
     1.8 +     val def = freezeT (get_thm theory (fid ^ "_def"))
     1.9       val dummy = if !trace then writeln ("DEF = " ^ string_of_thm def)
    1.10  	                   else ()
    1.11       (* val fconst = #lhs(S.dest_eq(concl def))  *)

     2.1 --- a/src/HOLCF/domain/theorems.ML	Thu Oct 21 18:45:55 1999 +0200
     2.2 +++ b/src/HOLCF/domain/theorems.ML	Thu Oct 21 18:46:33 1999 +0200
     2.3 @@ -75,7 +75,7 @@
     2.4  
     2.5  (* ----- getting the axioms and definitions --------------------------------- *)
     2.6  
     2.7 -local fun ga s dn = get_axiom thy (dn^"."^s) in
     2.8 +local fun ga s dn = get_thm thy (dn^"."^s) in
     2.9  val ax_abs_iso    = ga "abs_iso"  dname;
    2.10  val ax_rep_iso    = ga "rep_iso"  dname;
    2.11  val ax_when_def   = ga "when_def" dname;
    2.12 @@ -350,7 +350,7 @@
    2.13  
    2.14  (* ----- getting the composite axiom and definitions ------------------------ *)
    2.15  
    2.16 -local fun ga s dn = get_axiom thy (dn^"."^s) in
    2.17 +local fun ga s dn = get_thm thy (dn^"."^s) in
    2.18  val axs_reach      = map (ga "reach"     ) dnames;
    2.19  val axs_take_def   = map (ga "take_def"  ) dnames;
    2.20  val axs_finite_def = map (ga "finite_def") dnames;