--- a/src/HOL/Data_Structures/Trie_Fun.thy Wed Jun 03 11:44:21 2020 +0200
+++ b/src/HOL/Data_Structures/Trie_Fun.thy Thu Jun 04 15:30:22 2020 +0000
@@ -67,12 +67,11 @@
case 1 thus ?case by (force split: option.splits)
next
case 2
- thus ?case
- apply (auto simp add: image_iff split!: if_splits option.splits)
- apply blast
- apply (metis insertE insertI2 insert_Diff_single option.inject)
- apply blast
- by (metis insertE insertI2 insert_Diff_single option.inject)
+ show ?case
+ apply (auto simp add: image_iff 2 split!: if_splits option.splits)
+ apply (metis DiffI empty_iff insert_iff option.inject)
+ apply (metis DiffI empty_iff insert_iff option.inject)
+ done
qed
interpretation S: Set