separate session HOL-Mirabelle-ex -- cannot run isolated shell scripts within build tool;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/ex/Ex.thy	Sat Jul 28 20:36:25 2012 +0200
@@ -0,0 +1,12 @@
+theory Ex imports Pure
+begin
+
+ML {*
+  val rc = Isabelle_System.bash
+    "cd \"$ISABELLE_HOME/src/HOL/Library\"; \"$ISABELLE_TOOL\" mirabelle -q arith Inner_Product.thy";
+  if rc <> 0 then error ("Mirabelle example failed: " ^ string_of_int rc)
+  else ();
+*} -- "some arbitrary small test case"
+
+end
+

--- a/src/HOL/ROOT	Sat Jul 28 20:27:39 2012 +0200
+++ b/src/HOL/ROOT	Sat Jul 28 20:36:25 2012 +0200
@@ -605,9 +605,9 @@
 session Mirabelle = HOL +
   options [document = false]
   theories Mirabelle_Test
-(* FIXME
-	@cd Library; $(ISABELLE_TOOL) mirabelle -q arith Inner_Product.thy # some arbitrary small test case
-*)
+
+session ex in "Mirabelle/ex" = "HOL-Mirabelle" +
+  theories Ex
 
 session SMT_Examples = "HOL-Word" +
   options [document = false, quick_and_dirty]