equal
deleted
inserted
replaced
449 (* Type.tyenv -> Term.term -> Term.term *) |
449 (* Type.tyenv -> Term.term -> Term.term *) |
450 |
450 |
451 fun monomorphic_term typeSubs t = |
451 fun monomorphic_term typeSubs t = |
452 map_types (map_type_tvar |
452 map_types (map_type_tvar |
453 (fn v => |
453 (fn v => |
454 case Type.lookup (typeSubs, v) of |
454 case Type.lookup typeSubs v of |
455 NONE => |
455 NONE => |
456 (* schematic type variable not instantiated *) |
456 (* schematic type variable not instantiated *) |
457 raise REFUTE ("monomorphic_term", |
457 raise REFUTE ("monomorphic_term", |
458 "no substitution for type variable " ^ fst (fst v) ^ |
458 "no substitution for type variable " ^ fst (fst v) ^ |
459 " in term " ^ Display.raw_string_of_term t) |
459 " in term " ^ Display.raw_string_of_term t) |