# HG changeset patch # User wenzelm # Date 1704116168 -3600 # Node ID 9495bd0112d7b8d36b1cb06f8bccc4f0472d91cb # Parent 1c758cd8d5b2f7c509e1ae8249a17d02adb2dcbc clarified signature; diff -r 1c758cd8d5b2 -r 9495bd0112d7 src/HOL/Types_To_Sets/internalize_sort.ML --- a/src/HOL/Types_To_Sets/internalize_sort.ML Sun Dec 31 22:39:40 2023 +0100 +++ b/src/HOL/Types_To_Sets/internalize_sort.ML Mon Jan 01 14:36:08 2024 +0100 @@ -31,7 +31,8 @@ val thy = Thm.theory_of_thm thm; val tvar = Thm.typ_of ctvar; - val ({constraints, outer_constraints, ...}, _) = Logic.unconstrainT [] (Thm.prop_of thm); + val {constraints, outer_constraints, ...} = + Logic.unconstrain_context [] (Types.build (Thm.prop_of thm |> Types.add_atyps)); fun is_proper_class thy = can (Axclass.get_info thy); (* trick by FH *) fun reduce_to_non_proper_sort (TVar (name, sort)) = diff -r 1c758cd8d5b2 -r 9495bd0112d7 src/Pure/logic.ML --- a/src/Pure/logic.ML Sun Dec 31 22:39:40 2023 +0100 +++ b/src/Pure/logic.ML Mon Jan 01 14:36:08 2024 +0100 @@ -65,7 +65,8 @@ {typ_operation: {strip_sorts: bool} -> typ Same.operation, constraints: ((typ * class) * term) list, outer_constraints: (typ * class) list} - val unconstrainT: sort list -> term -> unconstrain_context * term + val unconstrain_context: sort Ord_List.T -> Types.set -> unconstrain_context + val unconstrainT: sort Ord_List.T -> term -> unconstrain_context * term val protectC: term val protect: term -> term val unprotect: term -> term @@ -365,9 +366,8 @@ constraints: ((typ * class) * term) list, outer_constraints: (typ * class) list}; -fun unconstrainT shyps prop = +fun unconstrain_context shyps present_set = let - val present_set = Types.build (prop |> (fold_types o fold_atyps) Types.add_set); val {present, extra} = present_sorts shyps present_set; val n = Types.size present_set; @@ -386,7 +386,7 @@ | NONE => (case AList.lookup (op =) constraints_map (Type.sort_of_atyp T) of SOME T' => T' |> strip_sorts ? Term.strip_sortsT - | NONE => raise TYPE ("Dangling type variable ", [T], [prop])))); + | NONE => raise TYPE ("Dangling type variable ", [T], [])))); val typ_operation = Term.map_atyps_same o atyp_operation; @@ -396,14 +396,18 @@ val outer_constraints = maps (fn (T, S) => map (pair T) S) (present @ map (`dummy_tfree) extra); + in + {typ_operation = typ_operation, + constraints = constraints, + outer_constraints = outer_constraints} + end; - val ucontext = - {typ_operation = typ_operation, - constraints = constraints, - outer_constraints = outer_constraints}; +fun unconstrainT shyps prop = + let + val ucontext = unconstrain_context shyps (Types.build (prop |> Types.add_atyps)); val prop' = prop - |> Term.map_types (typ_operation {strip_sorts = true}) - |> curry list_implies (map #2 constraints); + |> Term.map_types (#typ_operation ucontext {strip_sorts = true}) + |> curry list_implies (map #2 (#constraints ucontext)); in (ucontext, prop') end; diff -r 1c758cd8d5b2 -r 9495bd0112d7 src/Pure/term_items.ML --- a/src/Pure/term_items.ML Sun Dec 31 22:39:40 2023 +0100 +++ b/src/Pure/term_items.ML Mon Jan 01 14:36:08 2024 +0100 @@ -222,4 +222,16 @@ end; -structure Types = Term_Items(type key = typ val ord = Term_Ord.typ_ord); +structure Types: +sig + include TERM_ITEMS + val add_atyps: term -> set -> set +end = +struct + +structure Term_Items = Term_Items(type key = typ val ord = Term_Ord.typ_ord); +open Term_Items; + +val add_atyps = (fold_types o fold_atyps) add_set; + +end; diff -r 1c758cd8d5b2 -r 9495bd0112d7 src/Pure/thm.ML --- a/src/Pure/thm.ML Sun Dec 31 22:39:40 2023 +0100 +++ b/src/Pure/thm.ML Mon Jan 01 14:36:08 2024 +0100 @@ -1065,8 +1065,7 @@ fun lt (S1, S2) = le (S1, S2) andalso not (le (S2, S1)); fun rel (S1, S2) = if S1 = S2 then [] else [(Term.aT S1, S2)]; - val present_set = - Types.build (thm |> (fold_terms {hyps = true} o fold_types o fold_atyps) Types.add_set); + val present_set = Types.build (thm |> fold_terms {hyps = true} Types.add_atyps); val {present, extra} = Logic.present_sorts shyps present_set; val (witnessed, non_witnessed) =