--- a/src/Pure/term_xml.ML Tue Jul 12 15:32:16 2011 +0200
+++ b/src/Pure/term_xml.ML Tue Jul 12 17:53:06 2011 +0200
@@ -7,7 +7,6 @@
signature TERM_XML_OPS =
sig
type 'a T
- val indexname: indexname T
val sort: sort T
val typ: typ T
val term: term T
@@ -29,22 +28,20 @@
open XML.Encode;
-val indexname = pair string int;
-
val sort = list string;
fun typ T = T |> variant
- [fn Type x => pair string (list typ) x,
- fn TFree x => pair string sort x,
- fn TVar x => pair indexname sort x];
+ [fn Type (a, b) => ([a], (list typ) b),
+ fn TFree (a, b) => ([a], sort b),
+ fn TVar ((a, b), c) => ([a, int_atom b], sort c)];
fun term t = t |> variant
- [fn Const x => pair string typ x,
- fn Free x => pair string typ x,
- fn Var x => pair indexname typ x,
- fn Bound x => int x,
- fn Abs x => triple string typ term x,
- fn op $ x => pair term term x];
+ [fn Const (a, b) => ([a], typ b),
+ fn Free (a, b) => ([a], typ b),
+ fn Var ((a, b), c) => ([a, int_atom b], typ c),
+ fn Bound a => ([int_atom a], []),
+ fn Abs (a, b, c) => ([a], pair typ term (b, c)),
+ fn a $ b => ([], pair term term (a, b))];
end;
@@ -56,22 +53,20 @@
open XML.Decode;
-val indexname = pair string int;
-
val sort = list string;
fun typ T = T |> variant
- [Type o pair string (list typ),
- TFree o pair string sort,
- TVar o pair indexname sort];
+ [fn ([a], b) => Type (a, list typ b),
+ fn ([a], b) => TFree (a, sort b),
+ fn ([a, b], c) => TVar ((a, int_atom b), sort c)];
fun term t = t |> variant
- [Const o pair string typ,
- Free o pair string typ,
- Var o pair indexname typ,
- Bound o int,
- Abs o triple string typ term,
- op $ o pair term term];
+ [fn ([a], b) => Const (a, typ b),
+ fn ([a], b) => Free (a, typ b),
+ fn ([a, b], c) => Var ((a, int_atom b), typ c),
+ fn ([a], []) => Bound (int_atom a),
+ fn ([a], b) => let val (c, d) = pair typ term b in Abs (a, c, d) end,
+ fn ([], a) => op $ (pair term term a)];
end;