src/Pure/Tools/find_theorems.ML

       | app (r, consts, f :: fs) =
           let val (r', consts') = f (thm, consts)
           in app (opt_add r r', consts', fs) end;
   in app end;
 
- 
+
 in
 
 fun filter_criterion ctxt opt_goal (b, c) =
   (if b then I else (apfst opt_not)) o filter_crit ctxt opt_goal c;
 

     val start = start_timing ();
 
     val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
     val (foundo, thms) = find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria;
     val returned = length thms;
-    
+
     val tally_msg =
       (case foundo of
         NONE => "displaying " ^ string_of_int returned ^ " theorems"
       | SOME found =>
           "found " ^ string_of_int found ^ " theorems" ^