# HG changeset patch
# User wenzelm
# Date 1437245991 -7200
# Node ID cde2b5d084e69be558d553edf518fae50095f967
# Parent  4050b243fc6039d0d493c739325fd6eddce53993# Parent  02924903a6fd21f514b94a79a515e3aa883eb67e
merged

diff -r 02924903a6fd -r cde2b5d084e6 src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Sat Jul 18 20:54:56 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Sat Jul 18 20:59:51 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;