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