| changeset 21113 | 5b76e541cc0a |
| parent 21079 | 747d716e98d0 |
| child 21404 | eb85850d3eb7 |
--- a/src/HOL/ex/CodeEmbed.thy Tue Oct 31 09:28:55 2006 +0100 +++ b/src/HOL/ex/CodeEmbed.thy Tue Oct 31 09:28:56 2006 +0100 @@ -78,7 +78,7 @@ subsection {* Code serialization setup *} code_type "typ" and "term" - (SML target_atom "Term.typ" and target_atom "Term.term") + (SML "Term.typ" and "Term.term") code_const Type and TFix and Const and App and Fix