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))  *)