# HG changeset patch
# User haftmann
# Date 1258037324 -3600
# Node ID 6ea8a4cce9e7c175627b1df9bd31b1b4d79a80b1
# Parent  68e058d061f518c59a62f6606db6131d2619ccde
repaired broken code_const for term_of [String.literal]

diff -r 68e058d061f5 -r 6ea8a4cce9e7 src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Thu Nov 12 09:11:46 2009 +0100
+++ b/src/HOL/Code_Evaluation.thy	Thu Nov 12 15:48:44 2009 +0100
@@ -145,7 +145,7 @@
   (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))")
 
 code_const "term_of \<Colon> String.literal \<Rightarrow> term"
-  (Eval "HOLogic.mk'_message'_string")
+  (Eval "HOLogic.mk'_literal")
 
 code_reserved Eval HOLogic