equal
deleted
inserted
replaced
414 concl_prop |> map_aterms varify_noninducts |> close_form |
414 concl_prop |> map_aterms varify_noninducts |> close_form |
415 |> lambda (Free ind_x) |
415 |> lambda (Free ind_x) |
416 |> hackish_string_of_term ctxt |
416 |> hackish_string_of_term ctxt |
417 in |
417 in |
418 ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]", |
418 ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]", |
419 stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)] []) |
419 stature), th |> Rule_Insts.read_instantiate ctxt [((p_name, 0), p_inst)] []) |
420 end |
420 end |
421 |
421 |
422 fun type_match thy (T1, T2) = |
422 fun type_match thy (T1, T2) = |
423 (Sign.typ_match thy (T2, T1) Vartab.empty; true) |
423 (Sign.typ_match thy (T2, T1) Vartab.empty; true) |
424 handle Type.TYPE_MATCH => false |
424 handle Type.TYPE_MATCH => false |