diff --git a/Core_DOM/Core_SC_DOM/scope_components/Core_DOM_Heap_WF.thy b/Core_DOM/Core_SC_DOM/scope_components/Core_DOM_Heap_WF.thy
index e0362fa..7c16c10 100644
--- a/Core_DOM/Core_SC_DOM/scope_components/Core_DOM_Heap_WF.thy
+++ b/Core_DOM/Core_SC_DOM/scope_components/Core_DOM_Heap_WF.thy
@@ -3041,7 +3041,7 @@ proof -
     assume "is_node_ptr_kind ptr"
     then have ?thesis
       using \<open>known_ptr ptr\<close> \<open>ptr |\<in>| object_ptr_kinds h\<close>
-      apply(auto simp add: known_ptr_impl get_owner_document_def a_get_owner_document_tups_def)
+      apply(auto simp add: known_ptr_impl get_owner_document_def a_get_owner_document_tups_def)[1]
       apply(split invoke_splits, (rule conjI | rule impI)+)+
          apply(drule(1) known_ptr_not_document_ptr[folded known_ptr_impl])
          apply(drule(1) known_ptr_not_character_data_ptr)