diff -r b2c14b489e60 -r fbb655bf62d4 src/Tools/Haskell/Haskell.thy --- a/src/Tools/Haskell/Haskell.thy Sun Jul 14 17:56:54 2024 +0200 +++ b/src/Tools/Haskell/Haskell.thy Sun Jul 14 18:10:06 2024 +0200 @@ -2347,6 +2347,7 @@ | Bound Int | Abs (Name, Typ, Term) | App (Term, Term) + | OFCLASS (Typ, Name) deriving (Show, Eq, Ord) @@ -2681,7 +2682,8 @@ \case { Var (a, b) -> Just (indexname a, typ_body b); _ -> Nothing }, \case { Bound a -> Just ([], int a); _ -> Nothing }, \case { Abs (a, b, c) -> Just ([a], pair typ term (b, c)); _ -> Nothing }, - \case { App a -> Just ([], pair term term a); _ -> Nothing }] + \case { App a -> Just ([], pair term term a); _ -> Nothing }, + \case { OFCLASS (a, b) -> Just ([b], typ a); _ -> Nothing }] \ generate_file "Isabelle/Term_XML/Decode.hs" = \ @@ -2730,7 +2732,8 @@ \(a, b) -> Var (indexname a, typ_body b), \([], a) -> Bound (int a), \([a], b) -> let (c, d) = pair typ term b in Abs (a, c, d), - \([], a) -> App (pair term term a)] + \([], a) -> App (pair term term a), + \([a], b) -> OFCLASS (typ b, a)] \ generate_file "Isabelle/XML/Classes.hs" = \