diff -r ace45a11a45e -r bad75618fb82 src/HOL/Proofs/Extraction/Higman.thy
--- a/src/HOL/Proofs/Extraction/Higman.thy	Thu Jul 02 08:49:04 2020 +0000
+++ b/src/HOL/Proofs/Extraction/Higman.thy	Thu Jul 02 12:10:58 2020 +0000
@@ -58,6 +58,7 @@
   by (erule L.induct) iprover+
 
 lemma lemma2': "R a vs ws \<Longrightarrow> L as vs \<Longrightarrow> L (a # as) ws"
+  supply [[simproc del: defined_all]]
   apply (induct set: R)
   apply (erule L.cases)
   apply simp+
@@ -69,17 +70,19 @@
   done
 
 lemma lemma2: "R a vs ws \<Longrightarrow> good vs \<Longrightarrow> good ws"
+  supply [[simproc del: defined_all]]
   apply (induct set: R)
   apply iprover
   apply (erule good.cases)
   apply simp_all
   apply (rule good0)
   apply (erule lemma2')
-  apply assumption
+   apply assumption
   apply (erule good1)
   done
 
 lemma lemma3': "T a vs ws \<Longrightarrow> L as vs \<Longrightarrow> L (a # as) ws"
+  supply [[simproc del: defined_all]]
   apply (induct set: T)
   apply (erule L.cases)
   apply simp_all
@@ -93,6 +96,7 @@
   done
 
 lemma lemma3: "T a ws zs \<Longrightarrow> good ws \<Longrightarrow> good zs"
+  supply [[simproc del: defined_all]]
   apply (induct set: T)
   apply (erule good.cases)
   apply simp_all
@@ -107,6 +111,7 @@
   done
 
 lemma lemma4: "R a ws zs \<Longrightarrow> ws \<noteq> [] \<Longrightarrow> T a ws zs"
+  supply [[simproc del: defined_all]]
   apply (induct set: R)
   apply iprover
   apply (case_tac vs)