src/Pure/ProofGeneral/proof_general_pgip.ML

         val immed_thms_of_thy = filter_out NameSpace.is_qualified o thms_of_thy
         fun thy_prefix s = case space_explode NameSpace.separator s of
                                     x::_::_ => SOME x  (* String.find? *)
                                   | _ => NONE
         fun subthys_of_thy s =
-            foldl  (fn (NONE,xs) => xs | (SOME x,xs) => insert op= x xs) []
+            List.foldl  (fn (NONE,xs) => xs | (SOME x,xs) => insert op= x xs) []
                    (map thy_prefix (thms_of_thy s))
         fun subthms_of_thy thy =
             (case thy_prefix thy of
                  NONE => immed_thms_of_thy thy
                | SOME prf => filter (String.isPrefix (unprefix (prf ^ NameSpace.separator) thy))