equal
deleted
inserted
replaced
752 case try (find_index (curry op = tname o fst)) dts of |
752 case try (find_index (curry op = tname o fst)) dts of |
753 NONE => error "dtyp_no_of_typ: Illegal recursion" |
753 NONE => error "dtyp_no_of_typ: Illegal recursion" |
754 | SOME i => i |
754 | SOME i => i |
755 *} |
755 *} |
756 |
756 |
757 ML {* |
|
758 fun rename_vars fnctn thm = |
|
759 let |
|
760 val vars = Term.add_vars (prop_of thm) [] |
|
761 val nvars = map (Var o ((apfst o apfst) fnctn)) vars |
|
762 in |
|
763 Thm.certify_instantiate ([], (vars ~~ nvars)) thm |
|
764 end |
|
765 *} |
|
766 |
|
767 lemma not_in_union: "c \<notin> a \<union> b \<equiv> (c \<notin> a \<and> c \<notin> b)" |
757 lemma not_in_union: "c \<notin> a \<union> b \<equiv> (c \<notin> a \<and> c \<notin> b)" |
768 by auto |
758 by auto |
769 |
759 |
770 ML {* |
760 ML {* |
771 fun supports_tac perm = |
761 fun supports_tac perm = |