author | huffman |
Wed, 01 Aug 2007 19:59:12 +0200 | |
changeset 24121 | a93b0f4df838 |
parent 24120 | 2ce3945228d8 |
child 24122 | fc7f857d33c8 |
--- 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