55 val typ_vname = Type (Sign.intern_type thy "vname", []); |
55 val typ_vname = Type (Sign.intern_type thy "vname", []); |
56 val typ_class = Type (Sign.intern_type thy "class", []); |
56 val typ_class = Type (Sign.intern_type thy "class", []); |
57 val typ_sort = Type (Sign.intern_type thy "sort", []); |
57 val typ_sort = Type (Sign.intern_type thy "sort", []); |
58 val typ_typ = Type (Sign.intern_type thy "typ", []); |
58 val typ_typ = Type (Sign.intern_type thy "typ", []); |
59 val typ_term = Type (Sign.intern_type thy "term", []); |
59 val typ_term = Type (Sign.intern_type thy "term", []); |
60 val term_sort = HOList.term_list typ_class MLString.term_ml_string; |
60 val term_sort = HOLogic.mk_list MLString.term_ml_string typ_class; |
61 fun term_typ f (Type (tyco, tys)) = |
61 fun term_typ f (Type (tyco, tys)) = |
62 Const (const_Type, MLString.typ_ml_string --> HOList.typ_list typ_typ --> typ_typ) |
62 Const (const_Type, MLString.typ_ml_string --> HOLogic.listT typ_typ --> typ_typ) |
63 $ MLString.term_ml_string tyco $ HOList.term_list typ_typ (term_typ f) tys |
63 $ MLString.term_ml_string tyco $ HOLogic.mk_list (term_typ f) typ_typ tys |
64 | term_typ f (TFree v) = |
64 | term_typ f (TFree v) = |
65 f v; |
65 f v; |
66 fun term_term f g (Const (c, ty)) = |
66 fun term_term f g (Const (c, ty)) = |
67 Const (const_Const, MLString.typ_ml_string --> typ_typ --> typ_term) |
67 Const (const_Const, MLString.typ_ml_string --> typ_typ --> typ_term) |
68 $ MLString.term_ml_string c $ g ty |
68 $ MLString.term_ml_string c $ g ty |