src/HOL/Hyperreal/transfer.ML

--- a/src/HOL/Hyperreal/transfer.ML	Fri Oct 21 18:14:32 2005 +0200
+++ b/src/HOL/Hyperreal/transfer.ML	Fri Oct 21 18:14:34 2005 +0200
@@ -72,7 +72,7 @@
       , REPEAT_ALL_NEW (resolve_tac intros) 1
       , match_tac [reflexive_thm] 1 ]
   in
-    prove_goalw_cterm (ths @ refolds @ unfolds) ct (fn _ => tacs)
+    OldGoals.prove_goalw_cterm (ths @ refolds @ unfolds) ct (fn _ => tacs)
   end
 
 fun transfer_tac ths =