equal
deleted
inserted
replaced
808 fun add_lower_defs ctxt defs = |
808 fun add_lower_defs ctxt defs = |
809 let |
809 let |
810 val defs_pre_sym = map symmetric defs |
810 val defs_pre_sym = map symmetric defs |
811 val defs_atom = map atomize_thm defs_pre_sym |
811 val defs_atom = map atomize_thm defs_pre_sym |
812 val defs_all = flat (map (add_lower_defs_aux ctxt) defs_atom) |
812 val defs_all = flat (map (add_lower_defs_aux ctxt) defs_atom) |
813 val defs_sym = map (fn t => eq_reflection OF [t]) defs_all |
|
814 in |
813 in |
815 map Thm.varifyT defs_sym |
814 map Thm.varifyT defs_all |
816 end |
815 end |
817 *} |
816 *} |
818 |
817 |
819 text {* the proper way to do it *} |
818 text {* the proper way to do it *} |
820 ML {* |
819 ML {* |