author | traytel |
Mon, 10 Apr 2017 18:01:46 +0200 | |
changeset 65436 | 1fd2dca8eb60 |
parent 65435 | 378175f44328 |
child 65438 | f556a7a9080c |
--- a/src/HOL/Tools/BNF/bnf_comp.ML Fri Apr 07 21:17:18 2017 +0200 +++ b/src/HOL/Tools/BNF/bnf_comp.ML Mon Apr 10 18:01:46 2017 +0200 @@ -18,7 +18,10 @@ val DEADID_bnf: BNF_Def.bnf type comp_cache - type unfold_set + type unfold_set = + {map_unfolds: thm list, + set_unfoldss: thm list list, + rel_unfolds: thm list} val empty_comp_cache: comp_cache val empty_unfolds: unfold_set