--- 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')]);