# HG changeset patch
# User wenzelm
# Date 1541688596 -3600
# Node ID 7cc2d66a92a64c0d007b77f22bf877af97b09a66
# Parent  bd215c56cd96b9ccfab5d34ae0d9c2cbcbf73b03
proper ML expressions, without trailing semicolons;

diff -r bd215c56cd96 -r 7cc2d66a92a6 src/HOL/Decision_Procs/Cooper.thy
--- 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"
diff -r bd215c56cd96 -r 7cc2d66a92a6 src/HOL/Decision_Procs/Ferrack.thy
--- 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"
diff -r bd215c56cd96 -r 7cc2d66a92a6 src/HOL/Decision_Procs/MIR.thy
--- 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]