some parallel ML;

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