# 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'),