src/Pure/Tools/find_theorems.ML
changeset 31684 d5d830979a54
parent 31042 d452117ba564
child 31687 0d2f700fe5e7
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Wed Jun 17 15:00:19 2009 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Wed Jun 17 15:14:48 2009 +0200
     1.3 @@ -282,7 +282,7 @@
     1.4            in app (opt_add r r', consts', fs) end;
     1.5    in app end;
     1.6  
     1.7 - 
     1.8 +
     1.9  in
    1.10  
    1.11  fun filter_criterion ctxt opt_goal (b, c) =
    1.12 @@ -417,7 +417,7 @@
    1.13      val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
    1.14      val (foundo, thms) = find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria;
    1.15      val returned = length thms;
    1.16 -    
    1.17 +
    1.18      val tally_msg =
    1.19        (case foundo of
    1.20          NONE => "displaying " ^ string_of_int returned ^ " theorems"