src/Pure/Isar/attrib.ML

       in ((th', dyn'), (decls, context')) end);
 
 in
 
 fun partial_evaluation ctxt facts =
-  (facts, Context.Proof (Context_Position.set_visible false ctxt)) |->
+  (facts, Context.Proof ctxt) |->
     fold_map (fn ((b, more_atts), fact) => fn context =>
       let
         val (fact', (decls, context')) =
           (fact, ([], context)) |-> fold_map (fn (ths, atts) => fn res1 =>
             (ths, res1) |-> fold_map (fn th => fn res2 =>