equal
deleted
inserted
replaced
696 |
696 |
697 fun def_type ctxt = |
697 fun def_type ctxt = |
698 let val Mode {pattern, ...} = get_mode ctxt |
698 let val Mode {pattern, ...} = get_mode ctxt |
699 in Variable.def_type ctxt pattern end; |
699 in Variable.def_type ctxt pattern end; |
700 |
700 |
701 fun standard_infer_types ctxt ts = |
701 fun standard_infer_types ctxt = |
702 Type_Infer.infer_types ctxt (try (Consts.the_constraint (consts_of ctxt))) (def_type ctxt) ts |
702 Type_Infer.infer_types ctxt (try (Consts.the_constraint (consts_of ctxt))) (def_type ctxt); |
703 handle TYPE (msg, _, _) => error msg; |
|
704 |
703 |
705 local |
704 local |
706 |
705 |
707 fun standard_typ_check ctxt = |
706 fun standard_typ_check ctxt = |
708 map (cert_typ_mode (Type.get_mode ctxt) ctxt) #> |
707 map (cert_typ_mode (Type.get_mode ctxt) ctxt) #> |