src/HOL/Tools/BNF/bnf_comp.ML
changeset 65436 1fd2dca8eb60
parent 63837 fdf90aa59868
child 67091 1393c2340eec
     1.1 --- a/src/HOL/Tools/BNF/bnf_comp.ML	Fri Apr 07 21:17:18 2017 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_comp.ML	Mon Apr 10 18:01:46 2017 +0200
     1.3 @@ -18,7 +18,10 @@
     1.4    val DEADID_bnf: BNF_Def.bnf
     1.5  
     1.6    type comp_cache
     1.7 -  type unfold_set
     1.8 +  type unfold_set =
     1.9 +    {map_unfolds: thm list,
    1.10 +     set_unfoldss: thm list list,
    1.11 +     rel_unfolds: thm list}
    1.12  
    1.13    val empty_comp_cache: comp_cache
    1.14    val empty_unfolds: unfold_set