src/HOL/Hyperreal/transfer.ML
changeset 17985 d5d576b72371
parent 17956 369e2af8ee45
child 18708 4b3dadb4fe33
     1.1 --- a/src/HOL/Hyperreal/transfer.ML	Sat Oct 22 01:22:10 2005 +0200
     1.2 +++ b/src/HOL/Hyperreal/transfer.ML	Tue Oct 25 18:18:49 2005 +0200
     1.3 @@ -64,16 +64,14 @@
     1.4      val {intros,unfolds,refolds,consts} = TransferData.get thy
     1.5      val (_$_$t') = concl_of (Tactic.rewrite true unfolds (cterm_of thy t))
     1.6      val u = unstar_term consts t'
     1.7 -    val ct = cterm_of thy (Logic.mk_equals (t,u))
     1.8      val tacs =
     1.9 -      [ rewrite_goals_tac atomizers
    1.10 +      [ rewrite_goals_tac (ths @ refolds @ unfolds)
    1.11 +      , rewrite_goals_tac atomizers
    1.12        , match_tac [transitive_thm] 1
    1.13        , resolve_tac [transfer_start] 1
    1.14        , REPEAT_ALL_NEW (resolve_tac intros) 1
    1.15        , match_tac [reflexive_thm] 1 ]
    1.16 -  in
    1.17 -    OldGoals.prove_goalw_cterm (ths @ refolds @ unfolds) ct (fn _ => tacs)
    1.18 -  end
    1.19 +  in Goal.prove thy [] [] (Logic.mk_equals (t,u)) (fn _ => EVERY tacs) end
    1.20  
    1.21  fun transfer_tac ths =
    1.22      SUBGOAL (fn (t,i) =>