tuned;

--- 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'

--- a/src/HOL/Tools/functor.ML	Fri Jul 29 20:38:39 2016 +0200
+++ b/src/HOL/Tools/functor.ML	Sat Jul 30 21:10:02 2016 +0200
@@ -190,7 +190,7 @@
         (Variable.export_terms (Variable.auto_fixes input_mapper ctxt) ctxt) input_mapper) [])
       then ()
       else error ("Illegal locally free variable(s) in term: "
-        ^ Syntax.string_of_term ctxt input_mapper);;
+        ^ Syntax.string_of_term ctxt input_mapper);
     val mapper = singleton (Variable.polymorphic ctxt) input_mapper;
     val _ =
       if null (Term.add_tfreesT (fastype_of mapper) []) then ()