# HG changeset patch
# User haftmann
# Date 1177060897 -7200
# Node ID d12a9d75eee61cf646cc708b4df5b749fd085b84
# Parent  4899f06effc65c54cc231f368066c8bc14df4f7e
transfer_tac accepts also HOL equations as theorems

diff -r 4899f06effc6 -r d12a9d75eee6 src/HOL/Hyperreal/transfer.ML
--- a/src/HOL/Hyperreal/transfer.ML	Fri Apr 20 11:21:36 2007 +0200
+++ b/src/HOL/Hyperreal/transfer.ML	Fri Apr 20 11:21:37 2007 +0200
@@ -59,13 +59,14 @@
 fun transfer_thm_of ctxt ths t =
   let
     val thy = ProofContext.theory_of ctxt;
-    val {intros,unfolds,refolds,consts} = TransferData.get (Context.Proof ctxt)
-    val meta = LocalDefs.meta_rewrite_rule ctxt
+    val {intros,unfolds,refolds,consts} = TransferData.get (Context.Proof ctxt);
+    val meta = LocalDefs.meta_rewrite_rule ctxt;
+    val ths' = map meta ths;
     val unfolds' = map meta unfolds and refolds' = map meta refolds;
     val (_$_$t') = concl_of (MetaSimplifier.rewrite true unfolds' (cterm_of thy t))
     val u = unstar_term consts t'
     val tac =
-      rewrite_goals_tac (ths @ refolds' @ unfolds') THEN
+      rewrite_goals_tac (ths' @ refolds' @ unfolds') THEN
       ALLGOALS ObjectLogic.full_atomize_tac THEN
       match_tac [transitive_thm] 1 THEN
       resolve_tac [transfer_start] 1 THEN