# HG changeset patch
# User nipkow
# Date 1491899365 -7200
# Node ID f556a7a9080ce8a4a878bc54a5e7740b93554791
# Parent  1fd2dca8eb60b7c53d7fb232004246740d8d2391# Parent  b8fc7e2e1b35a54fb17acb5703619b7c12ce173b
merged

diff -r b8fc7e2e1b35 -r f556a7a9080c src/HOL/Tools/BNF/bnf_comp.ML
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Tue Apr 11 09:13:28 2017 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Tue Apr 11 10:29:25 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