clarified Isabelle/Haskell type Term, following Isabelle/Scala (see 446b887e23c7);
--- 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 }]
\<close>
generate_file "Isabelle/Term_XML/Decode.hs" = \<open>
@@ -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)]
\<close>
generate_file "Isabelle/XML/Classes.hs" = \<open>