| changeset 58310 | 91ea607a34d8 |
| parent 58152 | 6fe60a9a5bad |
| child 58334 | 7553a1bcecb7 |
--- a/src/HOL/Code_Evaluation.thy Thu Sep 11 19:26:59 2014 +0200 +++ b/src/HOL/Code_Evaluation.thy Thu Sep 11 19:32:36 2014 +0200 @@ -13,7 +13,7 @@ subsubsection {* Terms and class @{text term_of} *} -datatype_new "term" = dummy_term +datatype "term" = dummy_term definition Const :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where "Const _ _ = dummy_term"