TFL/tfl.sml

--- a/TFL/tfl.sml	Mon Mar 13 13:27:44 2000 +0100
+++ b/TFL/tfl.sml	Mon Mar 13 13:28:31 2000 +0100
@@ -381,7 +381,7 @@
 	                  (wfrec $ map_term_types poly_tvars R) 
 	              $ functional
      val def_term = mk_const_def (Theory.sign_of thy) (Name, Ty, wfrec_R_M)
-  in  PureThy.add_defs_i [Thm.no_attributes (def_name, def_term)] thy  end
+  in  #1 (PureThy.add_defs_i [Thm.no_attributes (def_name, def_term)] thy)  end
 end;
 
 
@@ -534,11 +534,11 @@
      val (Name,Ty) = dest_atom c
      val defn = mk_const_def (Theory.sign_of thy) 
                  (Name, Ty, S.list_mk_abs (args,rhs)) 
-     val theory =
+     val (theory, [def0]) =
        thy
        |> PureThy.add_defs_i 
             [Thm.no_attributes (fid ^ "_def", defn)]
-     val def = freezeT (get_thm theory (fid ^ "_def"))
+     val def = freezeT def0;
      val dummy = if !trace then writeln ("DEF = " ^ string_of_thm def)
 	                   else ()
      (* val fconst = #lhs(S.dest_eq(concl def))  *)