src/HOL/Hyperreal/transfer.ML
changeset 17956 369e2af8ee45
parent 17432 835647238122
child 17985 d5d576b72371
--- 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 =