# HG changeset patch
# User wenzelm
# Date 1629662309 -7200
# Node ID f0b2136e2204ec21a34c0b686e5cf8ba378a83d8
# Parent  25c672c324671a8ff0701be0d409ea087ebd782b
tuned signature: prefer existing Haskell operations;

diff -r 25c672c32467 -r f0b2136e2204 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Sun Aug 22 21:39:57 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy	Sun Aug 22 21:58:29 2021 +0200
@@ -221,8 +221,6 @@
 module Isabelle.Library (
   (|>), (|->), (#>), (#->),
 
-  the, the_default,
-
   fold, fold_rev, single, map_index, get_index, separate,
 
   StringLike, STRING (..), TEXT (..), BYTES (..),
@@ -258,17 +256,6 @@
 (f #-> g) x  = x |> f |-> g
 
 
-{- options -}
-
-the :: Maybe a -> a
-the (Just x) = x
-the Nothing = error "the Nothing"
-
-the_default :: a -> Maybe a -> a
-the_default x Nothing = x
-the_default _ (Just y) = y
-
-
 {- lists -}
 
 fold :: (a -> b -> b) -> [a] -> b -> b
@@ -1113,7 +1100,7 @@
   Range, no_range, no_range_position, range_position, range
 ) where
 
-import Data.Maybe (isJust)
+import Data.Maybe (isJust, fromMaybe)
 import qualified Isabelle.Properties as Properties
 import qualified Isabelle.Bytes as Bytes
 import qualified Isabelle.Value as Value
@@ -1220,10 +1207,10 @@
 {- markup properties -}
 
 get_string :: Properties.T -> Bytes -> Bytes
-get_string props name = the_default "" (Properties.get_value Just props name)
+get_string props name = fromMaybe "" (Properties.get_value Just props name)
 
 get_int :: Properties.T -> Bytes -> Int
-get_int props name = the_default 0 (Properties.get_value Value.parse_int props name)
+get_int props name = fromMaybe 0 (Properties.get_value Value.parse_int props name)
 
 of_properties :: Properties.T -> T
 of_properties props =
@@ -1412,6 +1399,8 @@
 )
 where
 
+import Data.Maybe (fromJust)
+
 import Isabelle.Library
 import Isabelle.Bytes (Bytes)
 import qualified Isabelle.Value as Value
@@ -1482,7 +1471,7 @@
 option f (Just x) = [node (f x)]
 
 variant :: [V a] -> T a
-variant fs x = [tagged (the (get_index (\f -> f x) fs))]
+variant fs x = [tagged (fromJust (get_index (\f -> f x) fs))]
 \<close>
 
 generate_file "Isabelle/XML/Decode.hs" = \<open>