
diff -r 07f7b158ef32 -r 5693a977a767 src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Thu Jul 29 16:14:06 2004 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy	Thu Jul 29 16:14:42 2004 +0200
@@ -7,7 +7,7 @@
 
 header{*Construction of Hyperreals Using Ultrafilters*}
 
-theory HyperDef = Filter + Real
+theory HyperDef = Filter + "../Real/Real"
 files ("fuf.ML"):  (*Warning: file fuf.ML refers to the name Hyperdef!*)
 
 




