--- a/src/Pure/logic.ML Fri Dec 29 20:01:04 2023 +0100
+++ b/src/Pure/logic.ML Fri Dec 29 20:18:58 2023 +0100
@@ -60,9 +60,7 @@
val dest_arity: term -> string * sort list * class
val dummy_tfree: sort -> typ
type unconstrain_context =
- {present_map: (typ * typ) list,
- constraints_map: (sort * typ) list,
- atyp_map: typ -> typ,
+ {atyp_map: typ -> typ,
map_atyps: typ -> typ,
constraints: ((typ * class) * term) list,
outer_constraints: (typ * class) list};
@@ -356,9 +354,7 @@
fun dummy_tfree S = TFree ("'dummy", S);
type unconstrain_context =
- {present_map: (typ * typ) list,
- constraints_map: (sort * typ) list,
- atyp_map: typ -> typ,
+ {atyp_map: typ -> typ,
map_atyps: typ -> typ,
constraints: ((typ * class) * term) list,
outer_constraints: (typ * class) list};
@@ -397,9 +393,7 @@
maps (fn (T, S) => map (pair T) S) (present_sorts @ map (`dummy_tfree) extra);
val ucontext =
- {present_map = present_map,
- constraints_map = constraints_map,
- atyp_map = atyp_map,
+ {atyp_map = atyp_map,
map_atyps = map_atyps,
constraints = constraints,
outer_constraints = outer_constraints};