# HG changeset patch
# User wenzelm
# Date 1140643122 -3600
# Node ID 9aff3d859d3991fdfff09339c861b922bfb6d750
# Parent  a3cf88213ea54064c79f2d8f676298951f2ccf5c
removed obsolete meta_conjunction_tr';

diff -r a3cf88213ea5 -r 9aff3d859d39 src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Wed Feb 22 22:18:41 2006 +0100
+++ b/src/Pure/Syntax/syn_trans.ML	Wed Feb 22 22:18:42 2006 +0100
@@ -364,17 +364,6 @@
     | _ => raise Match);
 
 
-(* meta conjunction *)
-
-fun meta_conjunction_tr' (*"all"*)
-      [Abs (_, _, Const ("==>", _) $
-        (Const ("==>", _) $ A $ (Const ("==>", _) $ B $ (Const ("_aprop", _) $ Bound 0))) $
-        (Const ("_aprop", _) $ Bound 0))] =
-      if Term.loose_bvar1 (A, 0) orelse Term.loose_bvar1 (B, 0) then raise Match
-      else Lexicon.const "_meta_conjunction" $ A $ B
-  | meta_conjunction_tr' (*"all"*) ts = raise Match;
-
-
 (* type reflection *)
 
 fun type_tr' show_sorts (*"TYPE"*) (Type ("itself", [T])) ts =
@@ -449,7 +438,7 @@
   [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr),
    ("_TYPE", type_tr), ("_DDDOT", dddot_tr),
    ("_index", index_tr)],
-  [("all", meta_conjunction_tr')],
+  [],
   [("_abs", abs_ast_tr'), ("_idts", idtyp_ast_tr' "_idts"),
    ("_pttrns", idtyp_ast_tr' "_pttrns"), ("==>", impl_ast_tr'),
    ("_index", index_ast_tr')]);