# HG changeset patch
# User traytel
# Date 1437142383 -7200
# Node ID 4050b243fc6039d0d493c739325fd6eddce53993
# Parent  6349a28af772ad33643c1dd54a79a05f57d5ef3a
forgotten selector

diff -r 6349a28af772 -r 4050b243fc60 src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Thu Jul 16 18:36:16 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Fri Jul 17 16:13:03 2015 +0200
@@ -82,6 +82,7 @@
   val rel_mono_strong0_of_bnf: bnf -> thm
   val rel_mono_strong_of_bnf: bnf -> thm
   val rel_refl_of_bnf: bnf -> thm
+  val rel_map_of_bnf: bnf -> thm list
   val rel_transfer_of_bnf: bnf -> thm
   val rel_eq_of_bnf: bnf -> thm
   val rel_flip_of_bnf: bnf -> thm
@@ -485,6 +486,7 @@
 val rel_mono_strong0_of_bnf = Lazy.force o #rel_mono_strong0 o #facts o rep_bnf;
 val rel_mono_strong_of_bnf = Lazy.force o #rel_mono_strong o #facts o rep_bnf;
 val rel_refl_of_bnf = Lazy.force o #rel_refl o #facts o rep_bnf;
+val rel_map_of_bnf = Lazy.force o #rel_map o #facts o rep_bnf;
 val rel_transfer_of_bnf = Lazy.force o #rel_transfer o #facts o rep_bnf;
 val rel_Grp_of_bnf = Lazy.force o #rel_Grp o #facts o rep_bnf;
 val rel_conversep_of_bnf = Lazy.force o #rel_conversep o #facts o rep_bnf;