equal
deleted
inserted
replaced
400 "----------- fun guh2theID ------------------------------"; |
400 "----------- fun guh2theID ------------------------------"; |
401 "----------- fun guh2theID ------------------------------"; |
401 "----------- fun guh2theID ------------------------------"; |
402 "----------- fun guh2theID ------------------------------"; |
402 "----------- fun guh2theID ------------------------------"; |
403 |
403 |
404 val guh = "thy_scri_ListG-thm-zip_Nil"; |
404 val guh = "thy_scri_ListG-thm-zip_Nil"; |
405 print_depth 999; |
405 print_depth 3; (*999*) |
406 take_fromto 1 4 (Symbol.explode guh); |
406 take_fromto 1 4 (Symbol.explode guh); |
407 take_fromto 5 9 (Symbol.explode guh); |
407 take_fromto 5 9 (Symbol.explode guh); |
408 val rest = takerest (9,(Symbol.explode guh)); |
408 val rest = takerest (9,(Symbol.explode guh)); |
409 |
409 |
410 separate "-" rest; |
410 separate "-" rest; |