# HG changeset patch
# User wenzelm
# Date 1165024327 -3600
# Node ID fa8a7de5da28a2406d6282acbca7cb566beb086c
# Parent  6f79647cf53662cbe4dd1afb90ec21f85a505eb8
added some support for embedded terms;

diff -r 6f79647cf536 -r fa8a7de5da28 src/Pure/Pure.thy
--- 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 =