# HG changeset patch
# User wenzelm
# Date 1703877538 -3600
# Node ID 0a94277a1d35358614da9fbe28a718560a3bc01c
# Parent  8c9cce335a3dad6d8830074809dfa26c87707620
clarified signature: suppress unused fields;

diff -r 8c9cce335a3d -r 0a94277a1d35 src/Pure/logic.ML
--- 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};