# HG changeset patch
# User wenzelm
# Date 1638445589 -3600
# Node ID 0597884e6e91f62e49435349440f38203985054b
# Parent  d54b3c96ee50e24f4b7339a294f51d0548eddf0d
tuned --- fewer IDE warnings;

diff -r d54b3c96ee50 -r 0597884e6e91 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Tue Nov 30 11:31:07 2021 +0100
+++ b/src/Tools/Haskell/Haskell.thy	Thu Dec 02 12:46:29 2021 +0100
@@ -322,7 +322,7 @@
         Just y -> Just (i, y)
 
 separate :: a -> [a] -> [a]
-separate s (x : (xs @ (_ : _))) = x : s : separate s xs
+separate s (x : xs@(_ : _)) = x : s : separate s xs
 separate _ xs = xs;
 
 
@@ -342,7 +342,7 @@
   space_explode :: Char -> String -> [String]
   space_explode c = Split.split (Split.dropDelims (Split.whenElt (== c)))
   trim_line :: String -> String
-  trim_line s = gen_trim_line (length s) ((!!) s) take s
+  trim_line s = gen_trim_line (length s) (s !!) take s
 
 instance StringLike Text where
   space_explode :: Char -> Text -> [Text]
@@ -699,10 +699,7 @@
 get props name = List.lookup name props
 
 get_value :: (Bytes -> Maybe a) -> T -> Bytes -> Maybe a
-get_value parse props name =
-  case get props name of
-    Nothing -> Nothing
-    Just s -> parse s
+get_value parse props name = maybe Nothing parse (get props name)
 
 put :: Entry -> T -> T
 put entry props = entry : remove (fst entry) props
@@ -2746,7 +2743,6 @@
 Type classes for XML data representation.
 -}
 
-{-# LANGUAGE TypeSynonymInstances #-}
 {-# LANGUAGE FlexibleInstances #-}
 
 module Isabelle.XML.Classes