src/HOL/ex/CodeEmbed.thy
changeset 20453 855f07fabd76
parent 20400 0ad2f3bbd4f0
child 21079 747d716e98d0
equal deleted inserted replaced
20452:6d8b29c7a960 20453:855f07fabd76
    75 *}
    75 *}
    76 
    76 
    77 
    77 
    78 subsection {* Code serialization setup *}
    78 subsection {* Code serialization setup *}
    79 
    79 
    80 code_typapp
    80 code_type "typ" and "term"
    81   "typ"  ml (target_atom "Term.typ")
    81   (SML target_atom "Term.typ" and target_atom "Term.term")
    82   "term" ml (target_atom "Term.term")
       
    83 
    82 
    84 code_constapp
    83 code_const Type and TFix
    85   Type  ml ("Term.Type (_, _)")
    84   and Const and App and Fix
    86   TFix  ml ("Term.TFree (_, _)")
    85   (SML "Term.Type (_, _)" and "Term.TFree (_, _)"
    87   Const ml ("Term.Const (_, _)")
    86     and "Term.Const (_, _)" and "Term.$ (_, _)" and "Term.Free (_, _)")
    88   App   ml ("Term.$ (_, _)")
       
    89   Fix   ml ("Term.Free (_, _)")
       
    90 
    87 
    91 end
    88 end