# HG changeset patch
# User wenzelm
# Date 1346656540 -7200
# Node ID c0e298d05026decf186e04c987c7be536307e464
# Parent  0f21fae06a402f1ed16537be7c533adbc97fad5d
some parallel ML;

diff -r 0f21fae06a40 -r c0e298d05026 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Sun Sep 02 21:24:33 2012 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Mon Sep 03 09:15:40 2012 +0200
@@ -5502,14 +5502,17 @@
 definition
   "problem4 = E (And (Ge (Sub (Bound 1) (Bound 0))) (Eq (Add (Floor (Bound 1)) (Floor (Neg (Bound 0))))))"
 
-ML {* @{code mircfrqe} @{code problem1} *}
-ML {* @{code mirlfrqe} @{code problem1} *}  
-ML {* @{code mircfrqe} @{code problem2} *}
-ML {* @{code mirlfrqe} @{code problem2} *}  
-ML {* @{code mircfrqe} @{code problem3} *}
-ML {* @{code mirlfrqe} @{code problem3} *}  
-ML {* @{code mircfrqe} @{code problem4} *}
-ML {* @{code mirlfrqe} @{code problem4} *}
+ML {*
+  Par_List.map (fn e => e ())
+   [fn () => @{code mircfrqe} @{code problem1},
+    fn () => @{code mirlfrqe} @{code problem1},
+    fn () => @{code mircfrqe} @{code problem2},
+    fn () => @{code mirlfrqe} @{code problem2},
+    fn () => @{code mircfrqe} @{code problem3},
+    fn () => @{code mirlfrqe} @{code problem3},
+    fn () => @{code mircfrqe} @{code problem4},
+    fn () => @{code mirlfrqe} @{code problem4}]
+*}
 
 (*code_reflect Mir
   functions mircfrqe mirlfrqe