src/HOL/Tools/try0.ML
changeset 56982 51d4189d95cf
parent 56850 13a7bca533a3
child 57918 f5d73caba4e5
--- a/src/HOL/Tools/try0.ML	Fri May 16 19:13:50 2014 +0200
+++ b/src/HOL/Tools/try0.ML	Fri May 16 19:13:50 2014 +0200
@@ -122,7 +122,7 @@
 
 fun generic_try0 mode timeout_opt quad st =
   let
-    val st = st |> Proof.map_context (silence_methods false);
+    val st = Proof.map_contexts (silence_methods false) st;
     fun trd (_, _, t) = t;
     fun par_map f =
       if mode = Normal then Par_List.map f #> map_filter I #> sort (int_ord o pairself trd)