# HG changeset patch # User wenzelm # Date 1702996065 -3600 # Node ID 5c534c60e11e4f15ba8e458607d555eced7b4db6 # Parent 0b1fd4445329574ded64e94408b24c2f2e848882 tuned; diff -r 0b1fd4445329 -r 5c534c60e11e src/Pure/thm.ML --- a/src/Pure/thm.ML Tue Dec 19 15:17:04 2023 +0100 +++ b/src/Pure/thm.ML Tue Dec 19 15:27:45 2023 +0100 @@ -405,18 +405,18 @@ val union_constraints = Ord_List.union constraint_ord; -fun insert_constraints thy (T, S) = - let - val ignored = - S = [] orelse - (case T of - TFree (_, S') => S = S' - | TVar (_, S') => S = S' - | _ => false); - in - if ignored then I - else Ord_List.insert constraint_ord {theory = thy, typ = smash_atyps T, sort = S} - end; +fun insert_constraints _ (_, []) = I + | insert_constraints thy (T, S) = + let + val ignored = + (case T of + TFree (_, S') => S = S' + | TVar (_, S') => S = S' + | _ => false); + in + if ignored then I + else Ord_List.insert constraint_ord {theory = thy, typ = smash_atyps T, sort = S} + end; fun insert_constraints_env thy env = let