changeset 31594 | a94aa5f045fb |
parent 31205 | 98370b26c2ce |
child 31746 | 75fe3304015c |
--- 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")