src/Pure/proof_general.ML
changeset 19482 9f11af8f7ef9
parent 19473 d87a8838afa4
child 19907 f552697b2f19
     1.1 --- a/src/Pure/proof_general.ML	Thu Apr 27 12:11:56 2006 +0200
     1.2 +++ b/src/Pure/proof_general.ML	Thu Apr 27 15:06:35 2006 +0200
     1.3 @@ -493,7 +493,7 @@
     1.4  in
     1.5  
     1.6  fun setup_present_hook () =
     1.7 -  Present.add_hook (fn _ => fn res => tell_thm_deps (List.concat (map #2 res)));
     1.8 +  Present.add_hook (fn _ => fn res => tell_thm_deps (maps #2 res));
     1.9  
    1.10  end;
    1.11  
    1.12 @@ -1456,7 +1456,7 @@
    1.13    "\n  '(" ^ space_implode "\n    " (map (quote o regexp_quote) strs) ^ "))\n";
    1.14  
    1.15  fun make_elisp_commands commands kind = defconst kind
    1.16 -  (commands |> List.mapPartial (fn (c, _, k, _) => if k = kind then SOME c else NONE));
    1.17 +  (commands |> map_filter (fn (c, _, k, _) => if k = kind then SOME c else NONE));
    1.18  
    1.19  fun make_elisp_syntax (keywords, commands) =
    1.20    ";;\n\