src/Pure/Syntax/syntax_trans.ML
changeset 81232 9867b5cf3f7a
parent 81202 243f6bec771c
child 81506 f76a5849b570
--- a/src/Pure/Syntax/syntax_trans.ML	Tue Oct 22 13:39:24 2024 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML	Tue Oct 22 19:26:40 2024 +0200
@@ -205,7 +205,7 @@
 fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix "_update" x, T), ts)
   | update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix "_update" x, T), ts)
   | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
-      if Term_Position.is_position ty then list_comb (c $ update_name_tr [t] $ ty, ts)
+      if Term_Position.detect_position ty then list_comb (c $ update_name_tr [t] $ ty, ts)
       else
         list_comb (c $ update_name_tr [t] $
           (Lexicon.fun_type $