# HG changeset patch # User wenzelm # Date 1703931929 -3600 # Node ID 1488e69fd2a15850dbca557653b9844f0f07413e # Parent 0a94277a1d35358614da9fbe28a718560a3bc01c tuned; diff -r 0a94277a1d35 -r 1488e69fd2a1 src/Pure/logic.ML --- a/src/Pure/logic.ML Fri Dec 29 20:18:58 2023 +0100 +++ b/src/Pure/logic.ML Sat Dec 30 11:25:29 2023 +0100 @@ -361,18 +361,17 @@ fun unconstrainT shyps prop = let - val present = Types.build (prop |> (fold_types o fold_atyps) Types.add_set); - val present_sorts = map (fn T => (T, Type.sort_of_atyp T)) (Types.list_set present); + val present_set = Types.build (prop |> (fold_types o fold_atyps) Types.add_set); + val present = map (fn T => (T, Type.sort_of_atyp T)) (Types.list_set present_set); + val extra = fold (Sorts.remove_sort o #2) present shyps; - val extra = fold (Sorts.remove_sort o #2) present_sorts shyps; - - val n = Types.size present; + val n = Types.size present_set; val (names1, names2) = Name.invent Name.context Name.aT (n + length extra) |> chop n; val present_map = - map2 (fn (T, S) => fn a => (T, TVar ((a, 0), S))) present_sorts names1; + map2 (fn (T, S) => fn a => (T, TVar ((a, 0), S))) present names1; val constraints_map = - map2 (fn (_, S) => fn a => (S, TVar ((a, 0), S))) present_sorts names1 @ + map2 (fn (_, S) => fn a => (S, TVar ((a, 0), S))) present names1 @ map2 (fn S => fn a => (S, TVar ((a, 0), S))) extra names2; fun atyp_map T = @@ -390,7 +389,7 @@ map (fn c => ((T, c), mk_of_class (TVar (ai, []), c))) S); val outer_constraints = - maps (fn (T, S) => map (pair T) S) (present_sorts @ map (`dummy_tfree) extra); + maps (fn (T, S) => map (pair T) S) (present @ map (`dummy_tfree) extra); val ucontext = {atyp_map = atyp_map,