--- a/src/Pure/Syntax/syn_trans.ML Fri Dec 01 19:43:57 2000 +0100
+++ b/src/Pure/Syntax/syn_trans.ML Fri Dec 01 19:44:15 2000 +0100
@@ -282,10 +282,12 @@
(* meta implication *)
fun impl_ast_tr' (*"==>"*) asts =
- (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);
+ 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);
(* type reflection *)