# HG changeset patch
# User bulwahn
# Date 1355677938 -3600
# Node ID ee090b5712f32b4569ccb7c7ed92ac412a15d429
# Parent  768a3fbe4149ddff7f7746032c6b0fb60d5ea230
reverting d466ebc27810 as the previous changeset should allow to run Find_Unused_Assms_Examples again

diff -r 768a3fbe4149 -r ee090b5712f3 src/HOL/ROOT
--- a/src/HOL/ROOT	Sun Dec 16 18:07:29 2012 +0100
+++ b/src/HOL/ROOT	Sun Dec 16 18:12:18 2012 +0100
@@ -804,8 +804,8 @@
     Quickcheck_Narrowing_Examples
 
 session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = HOL +
-  theories [condition = ISABELLE_FULL_TEST, quick_and_dirty]
-    (* Find_Unused_Assms_Examples FIXME *)
+  theories [condition = ISABELLE_FULL_TEST, timeout = 5400, quick_and_dirty]
+    Find_Unused_Assms_Examples
     Needham_Schroeder_No_Attacker_Example
     Needham_Schroeder_Guided_Attacker_Example
     Needham_Schroeder_Unguided_Attacker_Example