src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML
changeset 54823 a510fc40559c
parent 54815 4f6ec8754bf5
child 54824 4e58a38b330b
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Thu Dec 19 17:11:54 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Thu Dec 19 17:24:17 2013 +0100
@@ -15,6 +15,7 @@
 
   datatype play =
     Played of reconstructor * Time.time |
+    Not_Played of reconstructor |
     Play_Timed_Out of reconstructor * Time.time |
     Play_Failed of reconstructor
 
@@ -35,6 +36,7 @@
 
 datatype play =
   Played of reconstructor * Time.time |
+  Not_Played of reconstructor |
   Play_Timed_Out of reconstructor * Time.time |
   Play_Failed of reconstructor