diff -r a81ea5d3dd41 -r c4f1bf2acf4c src/HOL/Real/HahnBanach/ROOT.ML
--- a/src/HOL/Real/HahnBanach/ROOT.ML	Sat Dec 30 22:03:47 2000 +0100
+++ b/src/HOL/Real/HahnBanach/ROOT.ML	Sat Dec 30 22:13:18 2000 +0100
@@ -5,4 +5,4 @@
 The Hahn-Banach theorem for real vector spaces (Isabelle/Isar).
 *)
 
-time_use_thy "HahnBanach";
+with_path "../../Hyperreal" time_use_thy "HahnBanach";