src/HOL/Library/RBT_Mapping.thy
changeset 63649 e690d6f2185b
parent 63194 0b7bdb75f451
child 68484 59793df7f853
--- a/src/HOL/Library/RBT_Mapping.thy	Wed Aug 10 09:33:54 2016 +0200
+++ b/src/HOL/Library/RBT_Mapping.thy	Wed Aug 10 14:50:59 2016 +0200
@@ -43,7 +43,10 @@
 
 lemma map_entry_Mapping [code]:
   "Mapping.map_entry k f (Mapping t) = Mapping (RBT.map_entry k f t)"
-  apply (transfer fixing: t) by (case_tac "RBT.lookup t k") auto
+  apply (transfer fixing: t)
+  apply (case_tac "RBT.lookup t k")
+   apply auto
+  done
 
 lemma keys_Mapping [code]:
   "Mapping.keys (Mapping t) = set (RBT.keys t)"