diff -r 09c90fdcd9f2 -r cb1590accf3e src/Tools/8bit/isa-patches/HOL/HOL2.p
--- 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;