skolem :: FolFormula -> Set Name -> (FolFormula, Set Name)
skolem fm = skolem1 [] (pnf fm)

skolem1 :: [Name] -> FolFormula -> Set Name -> (FolFormula, Set Name)
skolem1 quantVars (Forall x p) funcs = (Forall x newFm, nameSet)
  where (newFm, nameSet) = skolem1 (x : quantVars) p funcs
skolem1 quantVars (Exists x p) funcs = skolem1 quantVars newFm (Set.insert newName funcs)
  where newName = variant "s" funcs
        newFm = subst (Map.singleton x (Fn newName (map Var quantVars))) p
skolem1 _ fm funcs = (fm, funcs)