# HG changeset patch # User wenzelm # Date 1184671159 -7200 # Node ID 8ad7131dbfcf9906b70cf59faa94d762e3b57aab # Parent 441148ca8323e276c3101ab70918909709516742 moved print_translations from Pure.thy to Syntax/syn_trans.ML; diff -r 441148ca8323 -r 8ad7131dbfcf src/Pure/Pure.thy --- a/src/Pure/Pure.thy Tue Jul 17 13:19:18 2007 +0200 +++ b/src/Pure/Pure.thy Tue Jul 17 13:19:19 2007 +0200 @@ -33,10 +33,6 @@ locale (open) meta_term_syntax = fixes meta_term :: "'a => prop" ("TERM _") -parse_translation {* - [("\<^fixed>meta_term", fn [t] => Const ("ProtoPure.term", dummyT --> propT) $ t)] -*} - lemmas [intro?] = termI @@ -45,10 +41,6 @@ locale (open) meta_conjunction_syntax = fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2) -parse_translation {* - [("\<^fixed>meta_conjunction", fn [t, u] => Logic.mk_conjunction (t, u))] -*} - lemma all_conjunction: includes meta_conjunction_syntax shows "(!!x. PROP A(x) && PROP B(x)) == ((!!x. PROP A(x)) && (!!x. PROP B(x)))" diff -r 441148ca8323 -r 8ad7131dbfcf src/Pure/Syntax/syn_trans.ML --- a/src/Pure/Syntax/syn_trans.ML Tue Jul 17 13:19:18 2007 +0200 +++ b/src/Pure/Syntax/syn_trans.ML Tue Jul 17 13:19:19 2007 +0200 @@ -147,12 +147,21 @@ | bigimpl_ast_tr (*"_bigimpl"*) asts = raise Ast.AST ("bigimpl_ast_tr", asts); -(* type reflection *) +(* meta conjunction *) + +fun conjunction_tr [t, u] = Lexicon.const "ProtoPure.conjunction" $ t $ u + | conjunction_tr ts = raise TERM ("conjunction_tr", ts); + + +(* type/term reflection *) fun type_tr (*"_TYPE"*) [ty] = Lexicon.const "_constrain" $ Lexicon.const "TYPE" $ (Lexicon.const "itself" $ ty) | type_tr (*"_TYPE"*) ts = raise TERM ("type_tr", ts); +fun term_tr [t] = Lexicon.const "ProtoPure.term" $ t + | term_tr ts = raise TERM ("term_tr", ts); + (* dddot *) @@ -453,8 +462,8 @@ ("_bigimpl", bigimpl_ast_tr), ("_indexdefault", indexdefault_ast_tr), ("_indexnum", indexnum_ast_tr), ("_indexvar", indexvar_ast_tr), ("_struct", struct_ast_tr)], [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr), - ("_TYPE", type_tr), ("_DDDOT", dddot_tr), - ("_index", index_tr)], + ("\\<^fixed>meta_conjunction", conjunction_tr), ("_TYPE", type_tr), + ("\\<^fixed>meta_term", term_tr), ("_DDDOT", dddot_tr), ("_index", index_tr)], ([]: (string * (term list -> term)) list), [("_abs", abs_ast_tr'), ("_idts", idtyp_ast_tr' "_idts"), ("_pttrns", idtyp_ast_tr' "_pttrns"), ("==>", impl_ast_tr'),