# HG changeset patch
# User haftmann
# Date 1201851358 -3600
# Node ID 377b7aa0b5b50ca6483f2593aec71f0e11c55873
# Parent  9830e7ffd5749907e4bd33105f7eee8936e2c891
<TERM> syntax

diff -r 9830e7ffd574 -r 377b7aa0b5b5 src/HOL/Library/Eval.thy
--- a/src/HOL/Library/Eval.thy	Fri Feb 01 08:32:26 2008 +0100
+++ b/src/HOL/Library/Eval.thy	Fri Feb 01 08:35:58 2008 +0100
@@ -308,6 +308,19 @@
            (Eval.evaluate_cmd some_name t)));
 *}
 
-hide (open) const Type TFree Const App dummy_term typ_of term_of
+print_translation {*
+let
+  val term = Const ("<TERM>", dummyT);
+  fun tr1' [_, _] = term;
+  fun tr2' [] = term;
+in
+  [(@{const_syntax Const}, tr1'),
+    (@{const_syntax App}, tr1'),
+    (@{const_syntax dummy_term}, tr2')]
+end
+*}
+
+hide (open) const Type TFree typ_of term_of
+hide const Const App dummy_term
 
 end