# HG changeset patch
# User wenzelm
# Date 918245419 -3600
# Node ID c31c0750963734de4e28731cd18b3c9453e38085
# Parent  e8bbe64861b88aa3c2d4586530b08c719f60aaa1
*** empty log message ***

diff -r e8bbe64861b8 -r c31c07509637 src/HOL/Real/Hyperreal/ROOT.ML
--- 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";
diff -r e8bbe64861b8 -r c31c07509637 src/ZF/ex/Primrec_defs.ML
--- 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 ***)