src/Tools/Haskell/Haskell.thy

 {-# LANGUAGE OverloadedStrings #-}
 
 module Isabelle.Name (
   Name,
   uu, uu_, aT,
-  clean_index, clean,
+  clean_index, clean, internal, skolem, is_internal, is_skolem,
   Context, declare, is_declared, context, make_context, variant
 )
 where
 
 import Data.Word (Word8)

 uu = "uu"
 uu_ = "uu_"
 aT = "'a"
 
 
-{- suffix for internal names -}
+{- internal names -- NB: internal subsumes skolem -}
 
 underscore :: Word8
 underscore = Bytes.byte '_'
+
+internal, skolem :: Name -> Name
+internal x = x <> "_"
+skolem x = x <> "__"
+
+is_internal, is_skolem :: Name -> Bool
+is_internal = Bytes.isSuffixOf "_"
+is_skolem = Bytes.isSuffixOf "__"
 
 clean_index :: Name -> (Name, Int)
 clean_index x =
   if Bytes.null x || Bytes.last x /= underscore then (x, 0)
   else