# HG changeset patch # User wenzelm # Date 874942288 -7200 # Node ID f0396ac63e12ec9c25b677d8079ffee99d308efd # Parent 3f7053bf423756bd88b88050397499d4acaed1cc tuned lambda_ast_tr, idtyp_ast_tr' to accomodate fix of idt/idts vs. pttrn/pttrns; diff -r 3f7053bf4237 -r f0396ac63e12 src/Pure/Syntax/syn_trans.ML --- 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')];