# HG changeset patch
# User wenzelm
# Date 1721381345 -7200
# Node ID 7849b6370425de5f330b09ea86f962908eb61cf6
# Parent  41957635424914a062b4f6818af7c6ded06b9af0
clarified signature, following zterm.ML;

diff -r 419576354249 -r 7849b6370425 src/Pure/term_xml.ML
--- a/src/Pure/term_xml.ML	Fri Jul 19 11:28:25 2024 +0200
+++ b/src/Pure/term_xml.ML	Fri Jul 19 11:29:05 2024 +0200
@@ -12,7 +12,6 @@
   val sort: sort T
   val typ: typ T
   val term_raw: term T
-  val typ_body: typ T
   val term: Consts.T -> term T
 end
 
@@ -47,12 +46,12 @@
   fn Abs (a, b, c) => ([a], pair typ term_raw (b, c)),
   fn op $ a => ([], pair term_raw term_raw a)];
 
-fun typ_body T = if T = dummyT then [] else typ T;
+fun var_type T = if T = dummyT then [] else typ T;
 
 fun term consts t = t |> variant
  [fn Const (a, b) => ([a], list typ (Consts.typargs consts (a, b))),
-  fn Free (a, b) => ([a], typ_body b),
-  fn Var (a, b) => (indexname a, typ_body b),
+  fn Free (a, b) => ([a], var_type b),
+  fn Var (a, b) => (indexname a, var_type b),
   fn Bound a => ([], int a),
   fn Abs (a, b, c) => ([a], pair typ (term consts) (b, c)),
   fn t as op $ a =>
@@ -87,13 +86,13 @@
   fn ([a], b) => let val (c, d) = pair typ term_raw b in Abs (a, c, d) end,
   fn ([], a) => op $ (pair term_raw term_raw a)];
 
-fun typ_body [] = dummyT
-  | typ_body body = typ body;
+fun var_type [] = dummyT
+  | var_type body = typ body;
 
 fun term consts body = body |> variant
  [fn ([a], b) => Const (a, Consts.instance consts (a, list typ b)),
-  fn ([a], b) => Free (a, typ_body b),
-  fn (a, b) => Var (indexname a, typ_body b),
+  fn ([a], b) => Free (a, var_type b),
+  fn (a, b) => Var (indexname a, var_type b),
   fn ([], a) => Bound (int a),
   fn ([a], b) => let val (c, d) = pair typ (term consts) b in Abs (a, c, d) end,
   fn ([], a) => op $ (pair (term consts) (term consts) a),
diff -r 419576354249 -r 7849b6370425 src/Pure/term_xml.scala
--- a/src/Pure/term_xml.scala	Fri Jul 19 11:28:25 2024 +0200
+++ b/src/Pure/term_xml.scala	Fri Jul 19 11:29:05 2024 +0200
@@ -25,13 +25,13 @@
         { case TFree(a, b) => (List(a), sort(b)) },
         { case TVar(a, b) => (indexname(a), sort(b)) }))
 
-    val typ_body: T[Typ] = (t: Typ) => if (t == dummyT) Nil else typ(t)
+    private val var_type: T[Typ] = (t: Typ) => if (t == dummyT) Nil else typ(t)
 
     def term: T[Term] =
       variant[Term](List(
         { case Const(a, b) => (List(a), list(typ)(b)) },
-        { case Free(a, b) => (List(a), typ_body(b)) },
-        { case Var(a, b) => (indexname(a), typ_body(b)) },
+        { case Free(a, b) => (List(a), var_type(b)) },
+        { case Var(a, b) => (indexname(a), var_type(b)) },
         { case Bound(a) => (Nil, int(a)) },
         { case Abs(a, b, c) => (List(a), pair(typ, term)(b, c)) },
         { case App(a, b) => (Nil, pair(term, term)(a, b)) },
@@ -53,13 +53,13 @@
         { case (List(a), b) => TFree(a, sort(b)) },
         { case (a, b) => TVar(indexname(a), sort(b)) }))
 
-    val typ_body: T[Typ] = { case Nil => dummyT case body => typ(body) }
+    private val var_type: T[Typ] = { case Nil => dummyT case body => typ(body) }
 
     def term: T[Term] =
       variant[Term](List(
         { case (List(a), b) => Const(a, list(typ)(b)) },
-        { case (List(a), b) => Free(a, typ_body(b)) },
-        { case (a, b) => Var(indexname(a), typ_body(b)) },
+        { case (List(a), b) => Free(a, var_type(b)) },
+        { case (a, b) => Var(indexname(a), var_type(b)) },
         { case (Nil, a) => Bound(int(a)) },
         { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
         { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) },
@@ -72,8 +72,8 @@
       def term: T[Term] =
         variant[Term](List(
           { case (List(a), b) => Const(a, list(typ)(b)) },
-          { case (List(a), b) => Free(a, env_type(a, typ_body(b))) },
-          { case (a, b) => Var(indexname(a), typ_body(b)) },
+          { case (List(a), b) => Free(a, env_type(a, var_type(b))) },
+          { case (a, b) => Var(indexname(a), var_type(b)) },
           { case (Nil, a) => Bound(int(a)) },
           { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
           { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) },
diff -r 419576354249 -r 7849b6370425 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Fri Jul 19 11:28:25 2024 +0200
+++ b/src/Tools/Haskell/Haskell.thy	Fri Jul 19 11:29:05 2024 +0200
@@ -2651,7 +2651,7 @@
 
 {-# LANGUAGE LambdaCase #-}
 
-module Isabelle.Term_XML.Encode (indexname, sort, typ, typ_body, term)
+module Isabelle.Term_XML.Encode (indexname, sort, typ, term)
 where
 
 import Isabelle.Library
@@ -2671,15 +2671,15 @@
     \case { TFree (a, b) -> Just ([a], sort b); _ -> Nothing },
     \case { TVar (a, b) -> Just (indexname a, sort b); _ -> Nothing }]
 
-typ_body :: T Typ
-typ_body ty = if is_dummyT ty then [] else typ ty
+var_type :: T Typ
+var_type ty = if is_dummyT ty then [] else typ ty
 
 term :: T Term
 term t =
   t |> variant
    [\case { Const (a, b) -> Just ([a], list typ b); _ -> Nothing },
-    \case { Free (a, b) -> Just ([a], typ_body b); _ -> Nothing },
-    \case { Var (a, b) -> Just (indexname a, typ_body b); _ -> Nothing },
+    \case { Free (a, b) -> Just ([a], var_type b); _ -> Nothing },
+    \case { Var (a, b) -> Just (indexname a, var_type 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 },
@@ -2698,7 +2698,7 @@
 
 {-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}
 
-module Isabelle.Term_XML.Decode (indexname, sort, typ, typ_body, term)
+module Isabelle.Term_XML.Decode (indexname, sort, typ, term)
 where
 
 import Isabelle.Library
@@ -2720,16 +2720,16 @@
    \([a], b) -> TFree (a, sort b),
    \(a, b) -> TVar (indexname a, sort b)]
 
-typ_body :: T Typ
-typ_body [] = dummyT
-typ_body body = typ body
+var_type :: T Typ
+var_type [] = dummyT
+var_type body = typ body
 
 term :: T Term
 term t =
   t |> variant
    [\([a], b) -> Const (a, list typ b),
-    \([a], b) -> Free (a, typ_body b),
-    \(a, b) -> Var (indexname a, typ_body b),
+    \([a], b) -> Free (a, var_type b),
+    \(a, b) -> Var (indexname a, var_type 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),