equal
deleted
inserted
replaced
128 (** Generating function variables for the case definition |
128 (** Generating function variables for the case definition |
129 Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **) |
129 Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **) |
130 |
130 |
131 (*The function variable for a single constructor*) |
131 (*The function variable for a single constructor*) |
132 fun add_case ((_, T, _), name, args, _) (opno, cases) = |
132 fun add_case ((_, T, _), name, args, _) (opno, cases) = |
133 if Lexicon.is_identifier name then |
133 if Symbol_Pos.is_identifier name then |
134 (opno, (Free (case_varname ^ "_" ^ name, T), args) :: cases) |
134 (opno, (Free (case_varname ^ "_" ^ name, T), args) :: cases) |
135 else |
135 else |
136 (opno + 1, (Free (case_varname ^ "_op_" ^ string_of_int opno, T), args) |
136 (opno + 1, (Free (case_varname ^ "_op_" ^ string_of_int opno, T), args) |
137 :: cases); |
137 :: cases); |
138 |
138 |