# HG changeset patch
# User huffman
# Date 1185991152 -7200
# Node ID a93b0f4df8386a85554101be49c19001cca182c2
# Parent  2ce3945228d86aaf3af65062c34fe971df8942f4
fix looping when applied to standard subgoals

diff -r 2ce3945228d8 -r a93b0f4df838 src/HOL/Hyperreal/transfer.ML
--- 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