equal
deleted
inserted
replaced
146 | ["true"] => ["false"] |
146 | ["true"] => ["false"] |
147 | [] => ["false"] |
147 | [] => ["false"] |
148 | _ => value) |
148 | _ => value) |
149 | NONE => (name, value) |
149 | NONE => (name, value) |
150 |
150 |
151 (* Ensure that type systems such as "simple!" and "mono_guards?" are handled |
151 (* Ensure that type systems such as "mono_simple!" and "mono_guards?" are |
152 correctly. *) |
152 handled correctly. *) |
153 fun implode_param [s, "?"] = s ^ "?" |
153 fun implode_param [s, "?"] = s ^ "?" |
154 | implode_param [s, "!"] = s ^ "!" |
154 | implode_param [s, "!"] = s ^ "!" |
155 | implode_param ss = space_implode " " ss |
155 | implode_param ss = space_implode " " ss |
156 |
156 |
157 structure Data = Theory_Data |
157 structure Data = Theory_Data |