author | haftmann |
Tue, 09 Jun 2009 22:59:53 +0200 | |
changeset 31594 | a94aa5f045fb |
parent 31517 | e8a64ab9fe99 |
child 31595 | bd2f7211a420 |
--- a/src/HOL/Code_Eval.thy Tue Jun 09 14:20:37 2009 +0200 +++ b/src/HOL/Code_Eval.thy Tue Jun 09 22:59:53 2009 +0200 @@ -129,7 +129,7 @@ (Eval "Term.term") code_const Const and App - (Eval "Term.Const/ (_, _)" and "Term.$/ (_, _)") + (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))") code_const "term_of \<Colon> String.literal \<Rightarrow> term" (Eval "HOLogic.mk'_message'_string")