changeset 65436 | 1fd2dca8eb60 |
parent 63837 | fdf90aa59868 |
child 67091 | 1393c2340eec |
--- 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