| changeset 56279 | b4d874f6c6be |
| parent 55837 | 154855d9a564 |
| child 58616 | 4257a7f2bf39 |
--- a/src/HOL/ex/ML.thy Tue Mar 25 16:11:00 2014 +0100 +++ b/src/HOL/ex/ML.thy Tue Mar 25 16:54:38 2014 +0100 @@ -121,7 +121,7 @@ term "factorial 4" -- "symbolic term" value "factorial 4" -- "evaluation via ML code generation in the background" -declare [[ML_trace]] +declare [[ML_source_trace]] ML {* @{term "factorial 4"} *} -- "symbolic term in ML" ML {* @{code "factorial"} *} -- "ML code from function specification"