src/HOL/Hyperreal/transfer.ML
changeset 17956 369e2af8ee45
parent 17432 835647238122
child 17985 d5d576b72371
     1.1 --- a/src/HOL/Hyperreal/transfer.ML	Fri Oct 21 18:14:32 2005 +0200
     1.2 +++ b/src/HOL/Hyperreal/transfer.ML	Fri Oct 21 18:14:34 2005 +0200
     1.3 @@ -72,7 +72,7 @@
     1.4        , REPEAT_ALL_NEW (resolve_tac intros) 1
     1.5        , match_tac [reflexive_thm] 1 ]
     1.6    in
     1.7 -    prove_goalw_cterm (ths @ refolds @ unfolds) ct (fn _ => tacs)
     1.8 +    OldGoals.prove_goalw_cterm (ths @ refolds @ unfolds) ct (fn _ => tacs)
     1.9    end
    1.10  
    1.11  fun transfer_tac ths =