equal
deleted
inserted
replaced
18 |
18 |
19 fun ml_val txt = ml_val_open [] NONE txt; |
19 fun ml_val txt = ml_val_open [] NONE txt; |
20 |
20 |
21 fun ml_pat (lhs, pat) = |
21 fun ml_pat (lhs, pat) = |
22 let |
22 let |
23 val pat' = implode (map (fn "\\<dots>" => "_" | s => s) (Symbol.explode pat)) |
23 val pat' = implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat)) |
24 in "val " ^ pat' ^ " = " ^ lhs end; |
24 in "val " ^ pat' ^ " = " ^ lhs end; |
25 |
25 |
26 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end"; |
26 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end"; |
27 fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option"; |
27 fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option"; |
28 |
28 |