# HG changeset patch
# User traytel
# Date 1499838755 -7200
# Node ID a5a24e1a6d6f15253e71ba30aeb70bec6b668aec
# Parent  c6714a9562aef0a7f7c7c4533f03d43094aa8f05
redundant since c6714a9562ae

diff -r c6714a9562ae -r a5a24e1a6d6f src/HOL/Library/Finite_Map.thy
--- a/src/HOL/Library/Finite_Map.thy	Tue Jul 11 21:36:42 2017 +0200
+++ b/src/HOL/Library/Finite_Map.thy	Wed Jul 12 07:52:35 2017 +0200
@@ -646,22 +646,6 @@
       rel: fmrel
   by auto
 
-text \<open>
-  Unfortunately, @{command lift_bnf} doesn't register the definitional theorems. We're doing it
-  manually below.
-\<close>
-
-local_setup \<open>fn lthy =>
-  let
-    val SOME bnf = BNF_Def.bnf_of lthy @{type_name fmap}
-  in
-    lthy
-    |> Local_Theory.note ((@{binding fmmap_def}, []), [BNF_Def.map_def_of_bnf bnf]) |> #2
-    |> Local_Theory.note ((@{binding fmran'_def}, []), BNF_Def.set_defs_of_bnf bnf) |> #2
-    |> Local_Theory.note ((@{binding fmrel_def}, []), [BNF_Def.rel_def_of_bnf bnf]) |> #2
-  end
-\<close>
-
 declare fmap.pred_mono[mono]
 
 context includes lifting_syntax begin