# HG changeset patch
# User blanchet
# Date 1282672534 -7200
# Node ID fcb0fe4c2f27d3ac53ea9622bf5c2e47b796f99c
# Parent  27378b4a776beebd7ef598c0cbeb9cd904a2cfa9
make Mirabelle happy

diff -r 27378b4a776b -r fcb0fe4c2f27 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Aug 24 19:19:28 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Aug 24 19:55:34 2010 +0200
@@ -293,7 +293,7 @@
 local
 
 datatype sh_result =
-  SH_OK of int * int * string list |
+  SH_OK of int * int * (string * bool) list |
   SH_FAIL of int * int |
   SH_ERROR
 
@@ -354,7 +354,9 @@
   in
     case result of
       SH_OK (time_isa, time_atp, names) =>
-        let fun get_thms name = (name, thms_of_name (Proof.context_of st) name)
+        let
+          fun get_thms (name, chained) =
+            ((name, chained), thms_of_name (Proof.context_of st) name)
         in
           change_data id inc_sh_success;
           change_data id (inc_sh_lemmas (length names));
@@ -442,7 +444,8 @@
     if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal
     then () else
     let
-      val named_thms = Unsynchronized.ref (NONE : (string * thm list) list option)
+      val named_thms =
+        Unsynchronized.ref (NONE : ((string * bool) * thm list) list option)
       val minimize = AList.defined (op =) args minimizeK
       val metis_ft = AList.defined (op =) args metis_ftK