# 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