equal
deleted
inserted
replaced
402 |> close_form |
402 |> close_form |
403 |> lambda (Free ind_x) |
403 |> lambda (Free ind_x) |
404 |> hackish_string_of_term ctxt |
404 |> hackish_string_of_term ctxt |
405 in |
405 in |
406 ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]", stature), |
406 ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]", stature), |
407 th |> Rule_Insts.read_instantiate ctxt [((p_name, 0), p_inst)] []) |
407 th |> Rule_Insts.read_instantiate ctxt [(((p_name, 0), Position.none), p_inst)] []) |
408 end |
408 end |
409 |
409 |
410 fun type_match thy (T1, T2) = |
410 fun type_match thy (T1, T2) = |
411 (Sign.typ_match thy (T2, T1) Vartab.empty; true) |
411 (Sign.typ_match thy (T2, T1) Vartab.empty; true) |
412 handle Type.TYPE_MATCH => false |
412 handle Type.TYPE_MATCH => false |