changeset 36960 | 01594f816e3a |
parent 36555 | 8ff45c2076da |
child 37321 | 9d7cfae95b30 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon May 17 15:11:25 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon May 17 23:54:15 2010 +0200 @@ -102,7 +102,7 @@ let val s = unyxml y in y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso not (is_long_identifier (perhaps (try (unprefix "?")) s))) orelse - OuterKeyword.is_keyword s) ? quote + Keyword.is_keyword s) ? quote end fun monomorphic_term subst t =