proper ML expressions, without trailing semicolons;

--- a/src/HOL/Decision_Procs/Cooper.thy	Thu Nov 08 14:58:04 2018 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy	Thu Nov 08 15:49:56 2018 +0100
@@ -2524,7 +2524,7 @@
       val ps = map_index swap bs;
       val t' = term_of_fm ps vs (@{code pa} (fm_of_term ps vs t));
     in Thm.cterm_of ctxt (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t'))) end
-end;
+end
 \<close>
 
 ML_file "cooper_tac.ML"

--- a/src/HOL/Decision_Procs/Ferrack.thy	Thu Nov 08 14:58:04 2018 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Thu Nov 08 15:49:56 2018 +0100
@@ -2543,7 +2543,7 @@
     val vs = Term.add_frees t [];
     val t' = (term_of_fm vs o @{code linrqe} o fm_of_term vs) t;
   in (Thm.cterm_of ctxt o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
-end;
+end
 \<close>
 
 ML_file "ferrack_tac.ML"

--- a/src/HOL/Decision_Procs/MIR.thy	Thu Nov 08 14:58:04 2018 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy	Thu Nov 08 15:49:56 2018 +0100
@@ -5682,7 +5682,7 @@
     val qe = if Config.get ctxt quick_and_dirty then @{code mircfrqe} else @{code mirlfrqe};
     val t' = term_of_fm vs (qe (fm_of_term vs t));
   in Thm.cterm_of ctxt (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t'))) end
-end;
+end
 \<close>
 
 lemmas iff_real_of_int = of_int_eq_iff [where 'a = real, symmetric]