equal
deleted
inserted
replaced
31 argument and returns an atom set. A NONE binding has to be on an |
31 argument and returns an atom set. A NONE binding has to be on an |
32 argument that is an atom or an atom set. |
32 argument that is an atom or an atom set. |
33 *) |
33 *) |
34 |
34 |
35 (* |
35 (* |
36 The overview of the generation of free variables: |
36 An overview of the generation of free variables: |
37 |
37 |
38 1) fv_bn functions are generated only for the non-recursive binds. |
38 1) fv_bn functions are generated only for the non-recursive binds. |
39 |
39 |
40 An fv_bn for a constructor is a union of values for the arguments: |
40 An fv_bn for a constructor is a union of values for the arguments: |
41 |
41 |
72 involve the given argument. For a paricular binding: |
72 involve the given argument. For a paricular binding: |
73 |
73 |
74 - for a binding function bn: bn x |
74 - for a binding function bn: bn x |
75 - for a recursive argument of type ty': fv_fy' x |
75 - for a recursive argument of type ty': fv_fy' x |
76 - for nominal datatype ty' return: fv_ty' x |
76 - for nominal datatype ty' return: fv_ty' x |
|
77 *) |
|
78 |
|
79 (* |
|
80 An overview of the generation of alpha-equivalence: |
77 *) |
81 *) |
78 |
82 |
79 ML {* |
83 ML {* |
80 fun is_atom thy typ = |
84 fun is_atom thy typ = |
81 Sign.of_sort thy (typ, @{sort at}) |
85 Sign.of_sort thy (typ, @{sort at}) |