equal
deleted
inserted
replaced
297 let |
297 let |
298 fun typ_error T msg = error ("Non-admissible type expression\n" ^ |
298 fun typ_error T msg = error ("Non-admissible type expression\n" ^ |
299 Sign.string_of_typ sign (typ_of_dtyp (orig_descr @ descr) sorts T) ^ "\n" ^ msg); |
299 Sign.string_of_typ sign (typ_of_dtyp (orig_descr @ descr) sorts T) ^ "\n" ^ msg); |
300 |
300 |
301 fun get_dt_descr T i tname dts = |
301 fun get_dt_descr T i tname dts = |
302 (case Symtab.lookup (dt_info, tname) of |
302 (case Symtab.curried_lookup dt_info tname of |
303 NONE => typ_error T (tname ^ " is not a datatype - can't use it in\ |
303 NONE => typ_error T (tname ^ " is not a datatype - can't use it in\ |
304 \ nested recursion") |
304 \ nested recursion") |
305 | (SOME {index, descr, ...}) => |
305 | (SOME {index, descr, ...}) => |
306 let val (_, vars, _) = valOf (assoc (descr, index)); |
306 let val (_, vars, _) = valOf (assoc (descr, index)); |
307 val subst = ((map dest_DtTFree vars) ~~ dts) handle UnequalLengths => |
307 val subst = ((map dest_DtTFree vars) ~~ dts) handle UnequalLengths => |