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 =