Updated for Isabelle2019.

Core_DOM/monads/CharacterDataMonad.thy

@@ -59,7 +59,7 @@ lemma character_data_ptr_kinds_M_reads:
   using node_ptr_kinds_M_reads
   apply(simp add: reads_def node_ptr_kinds_M_defs character_data_ptr_kinds_M_defs 
       character_data_ptr_kinds_def preserved_def)
-  by (metis (mono_tags, hide_lams) node_ptr_kinds_small old.unit.exhaust preserved_def)
+  by (smt node_ptr_kinds_small preserved_def unit_all_impI)
 
 global_interpretation l_dummy defines get_M\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a = "l_get_M.a_get_M get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a" .
 lemma get_M_is_l_get_M: "l_get_M get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a type_wf character_data_ptr_kinds"

Core_DOM/monads/DocumentMonad.thy

@@ -58,7 +58,7 @@ lemma document_ptr_kinds_M_reads:
 
   apply(simp add: reads_def object_ptr_kinds_M_defs document_ptr_kinds_M_defs 
       document_ptr_kinds_def preserved_def)
-  by (metis (mono_tags, hide_lams) object_ptr_kinds_preserved_small old.unit.exhaust preserved_def)
+  by (smt object_ptr_kinds_preserved_small preserved_def unit_all_impI)
 
 global_interpretation l_dummy defines get_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t = "l_get_M.a_get_M get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t" .
 lemma get_M_is_l_get_M: "l_get_M get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t type_wf document_ptr_kinds"

Core_DOM/monads/ElementMonad.thy

@@ -56,7 +56,7 @@ lemma element_ptr_kinds_M_reads:
   "reads (\<Union>element_ptr. {preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t element_ptr RObject.nothing)}) element_ptr_kinds_M h h'"
   apply(simp add: reads_def node_ptr_kinds_M_defs element_ptr_kinds_M_defs element_ptr_kinds_def
       node_ptr_kinds_M_reads preserved_def)
-  by (metis (mono_tags, hide_lams) node_ptr_kinds_small old.unit.exhaust preserved_def)
+  by (smt filter_fset node_ptr_kinds_small preserved_def unit_all_impI)
 
 global_interpretation l_dummy defines get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t = "l_get_M.a_get_M get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t" .
 lemma get_M_is_l_get_M: "l_get_M get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t type_wf element_ptr_kinds"

Core_DOM/monads/NodeMonad.thy

@@ -77,7 +77,7 @@ lemma node_ptr_kinds_M_reads:
   using object_ptr_kinds_M_reads
   apply(simp add: reads_def node_ptr_kinds_M_defs node_ptr_kinds_def
       object_ptr_kinds_M_reads preserved_def)
-  by (metis (mono_tags, hide_lams)  object_ptr_kinds_preserved_small old.unit.exhaust preserved_def)
+  by (smt object_ptr_kinds_preserved_small preserved_def unit_all_impI)
 
 global_interpretation l_put_M type_wf node_ptr_kinds get\<^sub>N\<^sub>o\<^sub>d\<^sub>e put\<^sub>N\<^sub>o\<^sub>d\<^sub>e 
   rewrites "a_get_M = get_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e"