changeset 58919 | 82a71046dce8 |
parent 58091 | ecf5826ba234 |
child 58928 | 23d0ffd48006 |
--- a/src/HOL/Tools/ATP/atp_util.ML Thu Nov 06 11:44:41 2014 +0100 +++ b/src/HOL/Tools/ATP/atp_util.ML Thu Nov 06 13:36:19 2014 +0100 @@ -140,7 +140,7 @@ let val s = unyxml y in y |> ((not (is_long_identifier (unquote_tvar s)) andalso not (is_long_identifier (unquery_var s))) orelse - Keyword.is_keyword s) ? quote + Keyword.is_keyword (Keyword.get_keywords ()) s) ? quote end fun string_of_ext_time (plus, time) =