# HG changeset patch
# User wenzelm
# Date 1630352705 -7200
# Node ID 736374547a7f4b50f0abe073129717721da91f0d
# Parent  a308ed696b58626ac93f02ba28744410aa7a0a3b
more Isabelle/Haskell operations;

diff -r a308ed696b58 -r 736374547a7f src/Tools/Haskell/Haskell.thy
--- 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)