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