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