equal
deleted
inserted
replaced
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 " ^ Sign.string_of_term CPure.thy t) |
460 | SOME typ => |
460 | SOME typ => |
461 typ)) t; |
461 typ)) t; |
462 |
462 |
463 (* ------------------------------------------------------------------------- *) |
463 (* ------------------------------------------------------------------------- *) |
464 (* specialize_type: given a constant 's' of type 'T', which is a subterm of *) |
464 (* specialize_type: given a constant 's' of type 'T', which is a subterm of *) |