src/HOL/Library/Pattern_Aliases.thy

--- a/src/HOL/Library/Pattern_Aliases.thy	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Library/Pattern_Aliases.thy	Fri Oct 15 19:25:31 2021 +0200
@@ -55,7 +55,7 @@
 fun as_typ a = a --> a --> a
 
 fun strip_all t =
-  case try Logic.dest_all t of
+  case try Logic.dest_all_global t of
     NONE => ([], t)
   | SOME (var, t) => apfst (cons var) (strip_all t)