added some support for embedded terms;

--- a/src/Pure/Pure.thy	Sat Dec 02 02:52:02 2006 +0100
+++ b/src/Pure/Pure.thy	Sat Dec 02 02:52:07 2006 +0100
@@ -26,6 +26,18 @@
 lemmas meta_allE = meta_spec [elim_format]
 
 
+subsection {* Embedded terms *}
+
+locale (open) meta_term_syntax =
+  fixes meta_term :: "'a => prop"  ("TERM _")
+
+parse_translation {*
+  [("\<^fixed>meta_term", fn [t] => Logic.mk_term t)]
+*}
+
+lemmas [intro?] = termI
+
+
 subsection {* Meta-level conjunction *}
 
 locale (open) meta_conjunction_syntax =