# HG changeset patch
# User wenzelm
# Date 940524393 -7200
# Node ID 0576dad973b1b91243c318148dae681311fd741e
# Parent  c5f735f7428c3fe9194fd795fce3b8acbbde7736
get_thm;

diff -r c5f735f7428c -r 0576dad973b1 TFL/tfl.sml
--- a/TFL/tfl.sml	Thu Oct 21 18:45:55 1999 +0200
+++ b/TFL/tfl.sml	Thu Oct 21 18:46:33 1999 +0200
@@ -538,7 +538,7 @@
        thy
        |> PureThy.add_defs_i 
             [Thm.no_attributes (fid ^ "_def", defn)]
-     val def = freezeT (get_axiom theory (fid ^ "_def"))
+     val def = freezeT (get_thm theory (fid ^ "_def"))
      val dummy = if !trace then writeln ("DEF = " ^ string_of_thm def)
 	                   else ()
      (* val fconst = #lhs(S.dest_eq(concl def))  *)
diff -r c5f735f7428c -r 0576dad973b1 src/HOLCF/domain/theorems.ML
--- a/src/HOLCF/domain/theorems.ML	Thu Oct 21 18:45:55 1999 +0200
+++ b/src/HOLCF/domain/theorems.ML	Thu Oct 21 18:46:33 1999 +0200
@@ -75,7 +75,7 @@
 
 (* ----- getting the axioms and definitions --------------------------------- *)
 
-local fun ga s dn = get_axiom thy (dn^"."^s) in
+local fun ga s dn = 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;
@@ -350,7 +350,7 @@
 
 (* ----- getting the composite axiom and definitions ------------------------ *)
 
-local fun ga s dn = get_axiom thy (dn^"."^s) in
+local fun ga s dn = 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;