Syntax: last premise of "_bigimpl" is wrapped with "_asm", to have a hook for
printing.

--- a/src/Pure/Syntax/ast.ML	Fri Dec 17 12:43:12 2004 +0100
+++ b/src/Pure/Syntax/ast.ML	Sat Dec 18 17:10:49 2004 +0100
@@ -23,8 +23,10 @@
   val pretty_rule: ast * ast -> Pretty.T
   val pprint_ast: ast -> pprint_args -> unit
   val fold_ast: string -> ast list -> ast
+  val fold_ast2: string -> string -> ast list -> ast
   val fold_ast_p: string -> ast list * ast -> ast
   val unfold_ast: string -> ast -> ast list
+  val unfold_ast2: string -> string -> ast -> ast list
   val unfold_ast_p: string -> ast -> ast list * ast
   val trace_ast: bool ref
   val stat_ast: bool ref
@@ -142,6 +144,9 @@
 
 fun fold_ast_p c = foldr (fn (x, xs) => Appl [Constant c, x, xs]);
 
+fun fold_ast2 _ _ [] = raise Match
+  | fold_ast2 _ c1 [y] = Appl [Constant c1, y]
+  | fold_ast2 c c1 (x :: xs) = Appl [Constant c, x, fold_ast2 c c1 xs];
 
 (* unfold asts *)
 
@@ -149,6 +154,12 @@
       if c = c' then x :: (unfold_ast c xs) else [y]
   | unfold_ast _ y = [y];
 
+fun unfold_ast2 c c1 (y as Appl [Constant c', x, xs]) =
+      if c = c' then x :: (unfold_ast2 c c1 xs) else [y]
+  | unfold_ast2 _ c1 (y as Appl [Constant c', x]) =
+      if c1 = c' then [x] else [y]
+  | unfold_ast2 _ _ y = [y];
+
 fun unfold_ast_p c (y as Appl [Constant c', x, xs]) =
       if c = c' then apfst (cons x) (unfold_ast_p c xs)
       else ([], y)

--- a/src/Pure/Syntax/mixfix.ML	Fri Dec 17 12:43:12 2004 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Sat Dec 18 17:10:49 2004 +0100
@@ -227,7 +227,7 @@
   ("",            "var => aprop",              Delimfix "_"),
   ("_DDDOT",      "aprop",                     Delimfix "..."),
   ("_aprop",      "aprop => prop",             Delimfix "PROP _"),
-  ("",            "prop => asms",              Delimfix "_"),
+  ("_asm",        "prop => asms",              Delimfix "_"),
   ("_asms",       "[prop, asms] => asms",      Delimfix "_;/ _"),
   ("_bigimpl",    "[asms, prop] => prop",      Mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
   ("_ofclass",    "[type, logic] => prop",     Delimfix "(1OFCLASS/(1'(_,/ _')))"),

--- a/src/Pure/Syntax/syn_trans.ML	Fri Dec 17 12:43:12 2004 +0100
+++ b/src/Pure/Syntax/syn_trans.ML	Sat Dec 18 17:10:49 2004 +0100
@@ -132,9 +132,14 @@
 (* meta implication *)
 
 fun bigimpl_ast_tr (*"_bigimpl"*) [asms, concl] =
+      Ast.fold_ast_p "==>" (Ast.unfold_ast2 "_asms" "_asm" asms, concl)
+  | bigimpl_ast_tr (*"_bigimpl"*) asts = raise Ast.AST ("bigimpl_ast_tr", asts);
+
+(*
+fun bigimpl_ast_tr (*"_bigimpl"*) [asms, concl] =
       Ast.fold_ast_p "==>" (Ast.unfold_ast "_asms" asms, concl)
   | bigimpl_ast_tr (*"_bigimpl"*) asts = raise Ast.AST ("bigimpl_ast_tr", asts);
-
+*)
 
 (* type reflection *)
 
@@ -348,9 +353,18 @@
   else
     (case Ast.unfold_ast_p "==>" (Ast.Appl (Ast.Constant "==>" :: asts)) of
       (asms as _ :: _ :: _, concl)
+        => Ast.Appl [Ast.Constant "_bigimpl", Ast.fold_ast2 "_asms" "_asm" asms, concl]
+    | _ => raise Match);
+
+(*
+fun impl_ast_tr' (*"==>"*) asts =
+  if TypeExt.no_brackets () then raise Match
+  else
+    (case Ast.unfold_ast_p "==>" (Ast.Appl (Ast.Constant "==>" :: asts)) of
+      (asms as _ :: _ :: _, concl)
         => Ast.Appl [Ast.Constant "_bigimpl", Ast.fold_ast "_asms" asms, concl]
     | _ => raise Match);
-
+*)
 
 (* meta conjunction *)