--- a/src/Tools/Haskell/Haskell.thy Mon Aug 30 21:41:37 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy Mon Aug 30 21:45:05 2021 +0200
@@ -2161,7 +2161,7 @@
module Isabelle.Name (
Name,
uu, uu_, aT,
- clean_index, clean, internal, skolem, is_internal, is_skolem,
+ clean_index, clean, internal, skolem, is_internal, is_skolem, dest_internal, dest_skolem,
Context, declare, is_declared, context, make_context, variant
)
where
@@ -2199,6 +2199,10 @@
is_internal = Bytes.isSuffixOf "_"
is_skolem = Bytes.isSuffixOf "__"
+dest_internal, dest_skolem :: Name -> Maybe Name
+dest_internal = Bytes.try_unsuffix "_"
+dest_skolem = Bytes.try_unsuffix "__"
+
clean_index :: Name -> (Name, Int)
clean_index x =
if Bytes.null x || Bytes.last x /= underscore then (x, 0)