equal
deleted
inserted
replaced
441 THEN' resolve_tac (HOLogic.conj_elims @{thm alpha1_transp_aux}) |
441 THEN' resolve_tac (HOLogic.conj_elims @{thm alpha1_transp_aux}) |
442 ) |
442 ) |
443 1 *}) |
443 1 *}) |
444 done*) |
444 done*) |
445 |
445 |
|
446 ML {* |
|
447 fun dtyp_no_of_typ _ (TFree (n, _)) = error "dtyp_no_of_typ: Illegal free" |
|
448 | dtyp_no_of_typ _ (TVar _) = error "dtyp_no_of_typ: Illegal schematic" |
|
449 | dtyp_no_of_typ dts (Type (tname, Ts)) = |
|
450 case try (find_index (curry op = tname o fst)) dts of |
|
451 NONE => error "dtyp_no_of_typ: Illegal recursion" |
|
452 | SOME i => i |
|
453 *} |
|
454 |
446 end |
455 end |