--- a/src/Tools/8bit/isa-patches/HOL/HOL2.p Fri Jul 12 20:43:12 1996 +0200
+++ b/src/Tools/8bit/isa-patches/HOL/HOL2.p Fri Jul 12 20:46:03 1996 +0200
@@ -1,20 +1,24 @@
local open Ast;
-fun bigimpl_ast_tr (*"Gbigimpl"*) [asms, concl] =
+fun Gbigimpl_ast_tr (*"Gbigimpl"*) [asms, concl] =
fold_ast_p "κλ" (unfold_ast "_asms" asms, concl)
- | bigimpl_ast_tr (*"Gbigimpl"*) asts = raise_ast "bigimpl_ast_tr" asts;
-fun impl_ast_tr' (*"κλ"*) asts =
+ | Gbigimpl_ast_tr (*"Gbigimpl"*) asts = raise_ast "bigimpl_ast_tr" asts;
+fun Glam_ast_tr (*"Glam"*) [idts, body] =
+ fold_ast_p "_abs" (unfold_ast "_idts" idts, body)
+ | Glam_ast_tr (*"Glam"*) asts = raise_ast "lambda_ast_tr" asts;
+
+fun Gimpl_ast_tr' (*"Gbigimpl"*) asts =
(case unfold_ast_p "κλ" (Appl (Constant "κλ" :: asts)) of
(asms as _ :: _ :: _, concl)
=> Appl [Constant "Gbigimpl", fold_ast "_asms" asms, concl]
| _ => raise Match);
-
in
-val parse_ast_translation = ("Gbigimpl", bigimpl_ast_tr)::
- ("Glam", fn asts => Appl (Constant "_abs" :: asts))::
+ val parse_ast_translation = ("Gbigimpl", Gbigimpl_ast_tr)::
+ ("Glam", Glam_ast_tr)::
parse_ast_translation;
-val print_ast_translation = ("κλ", impl_ast_tr')::
- ("_lambda", fn asts => Appl (Constant "Glam" :: asts)) ::
+ val print_ast_translation = ("κλ", Gimpl_ast_tr')::
+ ("_lambda", fn asts =>
+ Appl (Constant "Glam" :: asts)) ::
print_ast_translation;
end;