# HG changeset patch
# User wenzelm
# Date 1721558257 -7200
# Node ID 4e8845bbcd814003e3c436b85c0269e5a656404e
# Parent  9efbbad0a83450a136d85395a61e7db9fd251f27
clarified signature: more robust operations;

diff -r 9efbbad0a834 -r 4e8845bbcd81 src/Pure/name.ML
--- a/src/Pure/name.ML	Sat Jul 20 22:43:27 2024 +0200
+++ b/src/Pure/name.ML	Sun Jul 21 12:37:37 2024 +0200
@@ -26,6 +26,7 @@
   val build_context: (context -> context) -> context
   val make_context: string list -> context
   val declare: string -> context -> context
+  val declare_renamed: string * string -> context -> context
   val is_declared: context -> string -> bool
   val invent: context -> string -> int -> string list
   val invent_names: context -> string -> 'a list -> (string * 'a) list
@@ -102,6 +103,9 @@
 fun declare_renaming (x, x') (Context tab) =
   Context (Symtab.update (clean x, SOME (clean x')) tab);
 
+fun declare_renamed (x, x') =
+  clean x <> clean x' ? declare_renaming (x, x') #> declare x';
+
 fun is_declared (Context tab) = Symtab.defined tab;
 fun declared (Context tab) = Symtab.lookup tab;
 
@@ -145,9 +149,7 @@
         let
           val x0 = Symbol.bump_init x;
           val x' = vary x0;
-          val ctxt' = ctxt
-            |> x0 <> x' ? declare_renaming (x0, x')
-            |> declare x';
+          val ctxt' = ctxt |> declare_renamed (x0, x');
         in (x', ctxt') end;
   in (x' ^ replicate_string n "_", ctxt') end;
 
diff -r 9efbbad0a834 -r 4e8845bbcd81 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Sat Jul 20 22:43:27 2024 +0200
+++ b/src/Tools/Haskell/Haskell.thy	Sun Jul 21 12:37:37 2024 +0200
@@ -2175,7 +2175,7 @@
   Name,
   uu, uu_, aT,
   clean_index, clean, internal, skolem, is_internal, is_skolem, dest_internal, dest_skolem,
-  Context, declare, declare_renaming, is_declared, declared, context, make_context,
+  Context, declare, declare_renamed, is_declared, declared, context, make_context,
   variant, variant_list
 )
 where
@@ -2242,6 +2242,10 @@
 declare_renaming (x, x') (Context names) =
   Context (Map.insert (clean x) (Just (clean x')) names)
 
+declare_renamed :: (Name, Name) -> Context -> Context
+declare_renamed (x, x') =
+  (if clean x /= clean x' then declare_renaming (x, x') else id) #> declare x'
+
 is_declared :: Context -> Name -> Bool
 is_declared (Context names) x = Map.member x names
 
@@ -2289,9 +2293,7 @@
         let
           x0 = bump_init x
           x' = vary x0
-          ctxt' = ctxt
-            |> (if x0 /= x' then declare_renaming (x0, x') else id)
-            |> declare x'
+          ctxt' = ctxt |> declare_renamed (x0, x')
         in (x', ctxt')
   in (x' <> Bytes.pack (replicate n underscore), ctxt')