src/Tools/Haskell/Haskell.thy

 dummyT :: Typ
 dummyT = Type (\<open>\<^type_name>\<open>dummy\<close>\<close>, [])
 
 
 data Term =
-    Const (String, Typ)
+    Const (String, [Typ])
   | Free (String, Typ)
   | Var (Indexname, Typ)
   | Bound Int
   | Abs (String, Typ, Term)
   | App (Term, Term)

     \case { TVar ((a, b), c) -> Just ([a, int_atom b], sort c); _ -> Nothing }]
 
 term :: T Term
 term t =
   t |> variant
-   [\case { Const (a, b) -> Just ([a], typ b); _ -> Nothing },
+   [\case { Const (a, b) -> Just ([a], list typ b); _ -> Nothing },
     \case { Free (a, b) -> Just ([a], typ b); _ -> Nothing },
     \case { Var ((a, b), c) -> Just ([a, int_atom b], typ c); _ -> Nothing },
     \case { Bound a -> Just ([int_atom a], []); _ -> Nothing },
     \case { Abs (a, b, c) -> Just ([a], pair typ term (b, c)); _ -> Nothing },
     \case { App a -> Just ([], pair term term a); _ -> Nothing }]

    \([a, b], c) -> TVar ((a, int_atom b), sort c)]
 
 term :: T Term
 term t =
   t |> variant
-   [\([a], b) -> Const (a, typ b),
+   [\([a], b) -> Const (a, list typ b),
     \([a], b) -> Free (a, typ b),
     \([a, b], c) -> Var ((a, int_atom b), typ c),
     \([a], []) -> Bound (int_atom a),
     \([a], b) -> let (c, d) = pair typ term b in Abs (a, c, d),
     \([], a) -> App (pair term term a)]