# HG changeset patch
# User wenzelm
# Date 1165067965 -3600
# Node ID b822c7e61701346485a63901015b905db6303792
# Parent  03fe6d36e948c7e18dfc35a46d2a9ee63529927d
meta_term_syntax: proper operation on untyped preterms;

diff -r 03fe6d36e948 -r b822c7e61701 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sat Dec 02 11:33:08 2006 +0100
+++ b/src/Pure/Pure.thy	Sat Dec 02 14:59:25 2006 +0100
@@ -32,7 +32,7 @@
   fixes meta_term :: "'a => prop"  ("TERM _")
 
 parse_translation {*
-  [("\<^fixed>meta_term", fn [t] => Logic.mk_term t)]
+  [("\<^fixed>meta_term", fn [t] => Const ("ProtoPure.term", dummyT --> propT) $ t)]
 *}
 
 lemmas [intro?] = termI