# HG changeset patch # User kuncar # Date 1444347477 -7200 # Node ID 3933c0d7edc9d71e9c3a405eff321fb808d62acf # Parent 1190beb207629f2b251a1408ca251ed9bb45d199 right parenthesization diff -r 1190beb20762 -r 3933c0d7edc9 src/HOL/Tools/Transfer/transfer.ML --- a/src/HOL/Tools/Transfer/transfer.ML Thu Oct 08 23:40:27 2015 +0200 +++ b/src/HOL/Tools/Transfer/transfer.ML Fri Oct 09 01:37:57 2015 +0200 @@ -632,8 +632,8 @@ fun eq_tac ctxt = eq_rules_tac ctxt (get_relator_eq_raw ctxt) fun transfer_step_tac ctxt = - REPEAT_ALL_NEW (resolve_tac ctxt (get_transfer_raw ctxt) - THEN_ALL_NEW (DETERM o eq_rules_tac ctxt (get_relator_eq_raw ctxt))) + REPEAT_ALL_NEW (resolve_tac ctxt (get_transfer_raw ctxt)) + THEN_ALL_NEW (DETERM o eq_rules_tac ctxt (get_relator_eq_raw ctxt)) fun transfer_tac equiv ctxt i = let