equal
deleted
inserted
replaced
694 case try (find_index (curry op = tname o fst)) dts of |
694 case try (find_index (curry op = tname o fst)) dts of |
695 NONE => error "dtyp_no_of_typ: Illegal recursion" |
695 NONE => error "dtyp_no_of_typ: Illegal recursion" |
696 | SOME i => i |
696 | SOME i => i |
697 *} |
697 *} |
698 |
698 |
699 end |
699 ML {* |
|
700 fun rename_vars fnctn thm = |
|
701 let |
|
702 val vars = Term.add_vars (prop_of thm) [] |
|
703 val nvars = map (Var o ((apfst o apfst) fnctn)) vars |
|
704 in |
|
705 Thm.certify_instantiate ([], (vars ~~ nvars)) thm |
|
706 end |
|
707 *} |
|
708 |
|
709 end |