src/HOL/Tools/try0.ML

--- a/src/HOL/Tools/try0.ML	Thu Apr 16 13:48:10 2015 +0200
+++ b/src/HOL/Tools/try0.ML	Thu Apr 16 14:18:32 2015 +0200
@@ -154,7 +154,6 @@
 fun try0 timeout_opt = fst oo generic_try0 Normal timeout_opt;
 
 fun try0_trans quad =
-  Toplevel.unknown_proof o
   Toplevel.keep (K () o generic_try0 Normal (SOME default_timeout) quad o Toplevel.proof_of);
 
 fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) = (s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2);