--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Fri Jul 29 20:38:39 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Sat Jul 30 21:10:02 2016 +0200
@@ -433,7 +433,7 @@
EVERY' [rtac ctxt (o_apply RS trans RS ballI), etac ctxt (set_mp RS Abs_inverse),
assume_tac ctxt])
Abs_inverses)])
- (cts ~~ map2 mk_trans map_comp_ids map_congLs)] 1;;
+ (cts ~~ map2 mk_trans map_comp_ids map_congLs)] 1;
fun mk_mor_fold_tac ctxt cT ct fold_defs ex_mor mor =
(EVERY' (map (stac ctxt) fold_defs) THEN' EVERY' [rtac ctxt rev_mp, rtac ctxt ex_mor, rtac ctxt impI] THEN'