fix looping when applied to standard subgoals

--- a/src/HOL/Hyperreal/transfer.ML	Wed Aug 01 18:05:43 2007 +0200
+++ b/src/HOL/Hyperreal/transfer.ML	Wed Aug 01 19:59:12 2007 +0200
@@ -73,8 +73,11 @@
 fun transfer_tac ctxt ths =
     SUBGOAL (fn (t,i) =>
         (fn th =>
-            let val tr = transfer_thm_of ctxt ths t
-            in rewrite_goals_tac [tr] th end))
+            let
+              val tr = transfer_thm_of ctxt ths t
+              val (_$l$r) = concl_of tr;
+              val trs = if l aconv r then [] else [tr];
+            in rewrite_goals_tac trs th end))
 
 local