equal
deleted
inserted
replaced
37 fun TFree_tr [v, sort] = Lexicon.const @{const_syntax TFree} $ v $ sort |
37 fun TFree_tr [v, sort] = Lexicon.const @{const_syntax TFree} $ v $ sort |
38 | TFree_tr ts = raise TERM ("TFree_tr", ts); |
38 | TFree_tr ts = raise TERM ("TFree_tr", ts); |
39 fun Fun_tr [ty1, ty2] = Lexicon.const @{const_syntax Fun} $ ty1 $ ty2 |
39 fun Fun_tr [ty1, ty2] = Lexicon.const @{const_syntax Fun} $ ty1 $ ty2 |
40 | Fun_tr ts = raise TERM("Fun_tr", ts); |
40 | Fun_tr ts = raise TERM("Fun_tr", ts); |
41 in [ |
41 in [ |
42 ("\\<^fixed>pure_term_Type", Type_tr), |
42 ("\<^fixed>pure_term_Type", Type_tr), |
43 ("\\<^fixed>pure_term_TFree", TFree_tr), |
43 ("\<^fixed>pure_term_TFree", TFree_tr), |
44 ("\\<^fixed>pure_term_Fun", Fun_tr) |
44 ("\<^fixed>pure_term_Fun", Fun_tr) |
45 ] end |
45 ] end |
46 *} |
46 *} |
47 |
47 |
48 notation (output) |
48 notation (output) |
49 Type (infixl "{\<struct>}" 120) |
49 Type (infixl "{\<struct>}" 120) |