# HG changeset patch
# User wenzelm
# Date 1629906413 -7200
# Node ID 6dc7ff3269065089dcd7bbef2448dbcb752e02dd
# Parent  30e2e44baa572523489c417599004d2cae8baa2f
more Isabelle/Haskell operations;

diff -r 30e2e44baa57 -r 6dc7ff326906 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Wed Aug 25 17:27:40 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy	Wed Aug 25 17:46:53 2021 +0200
@@ -2116,7 +2116,7 @@
 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
@@ -2141,11 +2141,19 @@
 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)