--- a/src/HOL/Real/Hyperreal/ROOT.ML Fri Feb 05 21:06:24 1999 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-(* Title: HOL/Hyperreal/ROOT
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1998 University of Cambridge
-
-Construction of the Hyperreals using ultrafilters, by Jacques Fleuriot
-*)
-
-HOL_build_completed; (*Make examples fail if HOL did*)
-
-writeln"Root file for HOL/Hyperreal";
-
-set proof_timing;
-time_use_thy "Filter";
--- a/src/ZF/ex/Primrec_defs.ML Fri Feb 05 21:06:24 1999 +0100
+++ b/src/ZF/ex/Primrec_defs.ML Fri Feb 05 21:10:19 1999 +0100
@@ -7,7 +7,7 @@
*)
(*Theory TF redeclares map_type*)
-val map_type = Context.thm "List.map_type";
+val map_type = thm "List.map_type";
(** Useful special cases of evaluation ***)