1.1 --- a/src/Pure/Syntax/syn_trans.ML Wed Feb 22 22:18:41 2006 +0100
1.2 +++ b/src/Pure/Syntax/syn_trans.ML Wed Feb 22 22:18:42 2006 +0100
1.3 @@ -364,17 +364,6 @@
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 Term.loose_bvar1 (A, 0) orelse Term.loose_bvar1 (B, 0) 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 @@ -449,7 +438,7 @@
1.22 [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr),
1.23 ("_TYPE", type_tr), ("_DDDOT", dddot_tr),
1.24 ("_index", index_tr)],
1.25 - [("all", meta_conjunction_tr')],
1.26 + [],
1.27 [("_abs", abs_ast_tr'), ("_idts", idtyp_ast_tr' "_idts"),
1.28 ("_pttrns", idtyp_ast_tr' "_pttrns"), ("==>", impl_ast_tr'),
1.29 ("_index", index_ast_tr')]);