moved print_translations from Pure.thy to Syntax/syn_trans.ML;
authorwenzelm
Tue Jul 17 13:19:19 2007 +0200 (2007-07-17 ago)
changeset 238248ad7131dbfcf
parent 23823 441148ca8323
child 23825 e0372eba47b7
moved print_translations from Pure.thy to Syntax/syn_trans.ML;
src/Pure/Pure.thy
src/Pure/Syntax/syn_trans.ML
     1.1 --- a/src/Pure/Pure.thy	Tue Jul 17 13:19:18 2007 +0200
     1.2 +++ b/src/Pure/Pure.thy	Tue Jul 17 13:19:19 2007 +0200
     1.3 @@ -33,10 +33,6 @@
     1.4  locale (open) meta_term_syntax =
     1.5    fixes meta_term :: "'a => prop"  ("TERM _")
     1.6  
     1.7 -parse_translation {*
     1.8 -  [("\<^fixed>meta_term", fn [t] => Const ("ProtoPure.term", dummyT --> propT) $ t)]
     1.9 -*}
    1.10 -
    1.11  lemmas [intro?] = termI
    1.12  
    1.13  
    1.14 @@ -45,10 +41,6 @@
    1.15  locale (open) meta_conjunction_syntax =
    1.16    fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
    1.17  
    1.18 -parse_translation {*
    1.19 -  [("\<^fixed>meta_conjunction", fn [t, u] => Logic.mk_conjunction (t, u))]
    1.20 -*}
    1.21 -
    1.22  lemma all_conjunction:
    1.23    includes meta_conjunction_syntax
    1.24    shows "(!!x. PROP A(x) && PROP B(x)) == ((!!x. PROP A(x)) && (!!x. PROP B(x)))"
     2.1 --- a/src/Pure/Syntax/syn_trans.ML	Tue Jul 17 13:19:18 2007 +0200
     2.2 +++ b/src/Pure/Syntax/syn_trans.ML	Tue Jul 17 13:19:19 2007 +0200
     2.3 @@ -147,12 +147,21 @@
     2.4    | bigimpl_ast_tr (*"_bigimpl"*) asts = raise Ast.AST ("bigimpl_ast_tr", asts);
     2.5  
     2.6  
     2.7 -(* type reflection *)
     2.8 +(* meta conjunction *)
     2.9 +
    2.10 +fun conjunction_tr [t, u] = Lexicon.const "ProtoPure.conjunction" $ t $ u
    2.11 +  | conjunction_tr ts = raise TERM ("conjunction_tr", ts);
    2.12 +
    2.13 +
    2.14 +(* type/term reflection *)
    2.15  
    2.16  fun type_tr (*"_TYPE"*) [ty] =
    2.17        Lexicon.const "_constrain" $ Lexicon.const "TYPE" $ (Lexicon.const "itself" $ ty)
    2.18    | type_tr (*"_TYPE"*) ts = raise TERM ("type_tr", ts);
    2.19  
    2.20 +fun term_tr [t] = Lexicon.const "ProtoPure.term" $ t
    2.21 +  | term_tr ts = raise TERM ("term_tr", ts);
    2.22 +
    2.23  
    2.24  (* dddot *)
    2.25  
    2.26 @@ -453,8 +462,8 @@
    2.27     ("_bigimpl", bigimpl_ast_tr), ("_indexdefault", indexdefault_ast_tr),
    2.28     ("_indexnum", indexnum_ast_tr), ("_indexvar", indexvar_ast_tr), ("_struct", struct_ast_tr)],
    2.29    [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr),
    2.30 -   ("_TYPE", type_tr), ("_DDDOT", dddot_tr),
    2.31 -   ("_index", index_tr)],
    2.32 +   ("\\<^fixed>meta_conjunction", conjunction_tr), ("_TYPE", type_tr),
    2.33 +   ("\\<^fixed>meta_term", term_tr), ("_DDDOT", dddot_tr), ("_index", index_tr)],
    2.34    ([]: (string * (term list -> term)) list),
    2.35    [("_abs", abs_ast_tr'), ("_idts", idtyp_ast_tr' "_idts"),
    2.36     ("_pttrns", idtyp_ast_tr' "_pttrns"), ("==>", impl_ast_tr'),