more robust;
authorwenzelm
Tue, 22 Oct 2024 13:39:24 +0200
changeset 81231 808d940fa838
parent 81230 fdde6af19ba7
child 81232 9867b5cf3f7a
more robust;
src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Tue Oct 22 12:52:25 2024 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Tue Oct 22 13:39:24 2024 +0200
@@ -167,7 +167,11 @@
 (* binder notation *)
 
 val binder_stamp = stamp ();
-val binder_name = perhaps (try Lexicon.unmark_const) #> Lexicon.mark_binder;
+
+fun binder_name c =
+  (if Lexicon.is_const c then Lexicon.unmark_const c
+   else if Lexicon.is_fixed c then Lexicon.unmark_fixed c
+   else c) |> Lexicon.mark_binder;
 
 val binder_bg = Symbol_Pos.explode0 "(";
 val binder_en = Symbol_Pos.explode0 "_./ _)";