equal
deleted
inserted
replaced
116 val bootstrap_thys = ["Bootstrap_Pure", "Bootstrap_ML_Bootstrap"]; |
116 val bootstrap_thys = ["Bootstrap_Pure", "Bootstrap_ML_Bootstrap"]; |
117 |
117 |
118 fun is_base_name s = |
118 fun is_base_name s = |
119 s <> "" andalso not (exists_string (member (op =) ["/", "\\", ":"]) s) |
119 s <> "" andalso not (exists_string (member (op =) ["/", "\\", ":"]) s) |
120 |
120 |
121 val import_name = Path.base_name o Path.explode; |
121 fun import_name s = |
|
122 if String.isSuffix ".thy" s then |
|
123 error ("Malformed theory import: " ^ quote s) |
|
124 else Path.base_name (Path.explode s); |
122 |
125 |
123 |
126 |
124 (* header args *) |
127 (* header args *) |
125 |
128 |
126 local |
129 local |