1.1 --- a/src/Pure/Syntax/syn_trans.ML	Sun Nov 11 21:38:04 2001 +0100
     1.2 +++ b/src/Pure/Syntax/syn_trans.ML	Sun Nov 11 21:38:25 2001 +0100
     1.3 @@ -302,6 +302,17 @@
     1.4      | _ => raise Match);
     1.5  
     1.6  
     1.7 +(* meta conjunction *)
     1.8 +
     1.9 +fun meta_conjunction_tr' (*"all"*)
    1.10 +      [Abs (_, _, Const ("==>", _) $
    1.11 +        (Const ("==>", _) $ A $ (Const ("==>", _) $ B $ (Const ("_aprop", _) $ Bound 0))) $
    1.12 +        (Const ("_aprop", _) $ Bound 0))] =
    1.13 +      if 0 mem_int Term.loose_bnos A orelse 0 mem_int Term.loose_bnos B then raise Match
    1.14 +      else Lexicon.const "_meta_conjunction" $ A $ B
    1.15 +  | meta_conjunction_tr' (*"all"*) ts = raise Match;
    1.16 +
    1.17 +
    1.18  (* type reflection *)
    1.19  
    1.20  fun type_tr' show_sorts (*"TYPE"*) (Type ("itself", [T])) ts =
    1.21 @@ -354,7 +365,7 @@
    1.22     ("_indexvar", indexvar_ast_tr)],
    1.23    [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr),
    1.24     ("_TYPE", type_tr), ("_DDDOT", dddot_tr), ("_K", k_tr)],
    1.25 -  []: (string * (term list -> term)) list,
    1.26 +  [("all", meta_conjunction_tr')],
    1.27    [("_abs", abs_ast_tr'), ("_idts", idtyp_ast_tr' "_idts"),
    1.28     ("_pttrns", idtyp_ast_tr' "_pttrns"), ("==>", impl_ast_tr')]);
    1.29