# HG changeset patch # User wenzelm # Date 1564393085 -7200 # Node ID 99024c9c83f69330e00a73dd37ce997e46349814 # Parent fdbb0c2e0162469ce1a80b0711f0377c1ef5225d proper constrains_map -- for shyps that are covered by present variables (amending 251f1fb44ccd); diff -r fdbb0c2e0162 -r 99024c9c83f6 src/Pure/logic.ML --- a/src/Pure/logic.ML Mon Jul 29 11:21:41 2019 +0200 +++ b/src/Pure/logic.ML Mon Jul 29 11:38:05 2019 +0200 @@ -58,7 +58,7 @@ val dest_arity: term -> string * sort list * class type unconstrain_context = {present_map: (typ * typ) list, - extra_map: (sort * typ) list, + constraints_map: (sort * typ) list, atyp_map: typ -> typ, map_atyps: typ -> typ, constraints: ((typ * class) * term) list, @@ -347,7 +347,7 @@ type unconstrain_context = {present_map: (typ * typ) list, - extra_map: (sort * typ) list, + constraints_map: (sort * typ) list, atyp_map: typ -> typ, map_atyps: typ -> typ, constraints: ((typ * class) * term) list, @@ -363,19 +363,18 @@ val present_map = map2 (fn (T, S) => fn a => (T, TVar ((a, 0), S))) present names1; - val extra_map = + val constraints_map = + 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 = (case AList.lookup (op =) present_map T of SOME U => U | NONE => - (case AList.lookup (op =) extra_map (Type.sort_of_atyp T) of + (case AList.lookup (op =) constraints_map (Type.sort_of_atyp T) of SOME U => U | NONE => raise TYPE ("Dangling type variable", [T], []))); - val constraints_map = - map2 (fn (_, S) => fn a => (S, TVar ((a, 0), S))) present names1 @ extra_map; val constraints = constraints_map |> maps (fn (_, T as TVar (ai, S)) => map (fn c => ((T, c), mk_of_class (TVar (ai, []), c))) S); @@ -387,7 +386,7 @@ val map_atyps = Term.map_atyps (Type.strip_sorts o atyp_map); val ucontext = {present_map = present_map, - extra_map = extra_map, + constraints_map = constraints_map, atyp_map = atyp_map, map_atyps = map_atyps, constraints = constraints,