
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 }]
 \<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>




