--- a/src/Pure/Syntax/syn_trans.ML Mon Sep 22 17:29:42 1997 +0200
+++ b/src/Pure/Syntax/syn_trans.ML Mon Sep 22 17:31:28 1997 +0200
@@ -61,8 +61,8 @@
fun idtyp_ast_tr (*"_idtyp"*) [x, ty] = Appl [Constant constrainC, x, ty]
| idtyp_ast_tr (*"_idtyp"*) asts = raise_ast "idtyp_ast_tr" asts;
-fun lambda_ast_tr (*"_lambda"*) [idts, body] =
- fold_ast_p "_abs" (unfold_ast "_idts" idts, body)
+fun lambda_ast_tr (*"_lambda"*) [pats, body] =
+ fold_ast_p "_abs" (unfold_ast "_pttrns" pats, body)
| lambda_ast_tr (*"_lambda"*) asts = raise_ast "lambda_ast_tr" asts;
val constrainAbsC = "_constrainAbs";
@@ -174,7 +174,7 @@
fun abs_ast_tr' (*"_abs"*) asts =
(case unfold_ast_p "_abs" (Appl (Constant "_abs" :: asts)) of
([], _) => raise_ast "abs_ast_tr'" asts
- | (xs, body) => Appl [Constant "_lambda", fold_ast "_idts" xs, body]);
+ | (xs, body) => Appl [Constant "_lambda", fold_ast "_pttrns" xs, body]);
(* binder *)
@@ -200,13 +200,13 @@
end;
-(* idts *)
+(* idtyp constraints *)
-fun idts_ast_tr' (*"_idts"*) [Appl [Constant c, x, ty], xs] =
+fun idtyp_ast_tr' a [Appl [Constant c, x, ty], xs] =
if c = constrainC then
- Appl [Constant "_idts", Appl [Constant "_idtyp", x, ty], xs]
+ Appl [Constant a, Appl [Constant "_idtyp", x, ty], xs]
else raise Match
- | idts_ast_tr' (*"_idts"*) _ = raise Match;
+ | idtyp_ast_tr' _ _ = raise Match;
(* meta propositions *)
@@ -281,7 +281,8 @@
[("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr),
("_K", k_tr)],
[],
- [("_abs", abs_ast_tr'), ("_idts", idts_ast_tr'), ("==>", impl_ast_tr')]);
+ [("_abs", abs_ast_tr'), ("_idts", idtyp_ast_tr' "_idts"),
+ ("_pttrns", idtyp_ast_tr' "_pttrns"), ("==>", impl_ast_tr')]);
val pure_trfunsT =
[("_mk_ofclass", mk_ofclass_tr'), ("_mk_ofclassS", mk_ofclassS_tr')];