--- a/src/Pure/Thy/thy_syn.ML Fri Feb 16 17:24:51 1996 +0100
+++ b/src/Pure/Thy/thy_syn.ML Fri Feb 16 18:00:47 1996 +0100
@@ -6,26 +6,25 @@
*)
signature THY_SYN_DATA =
-sig
+ sig
val user_keywords: string list
val user_sections: (string * (ThyParse.token list -> (string * string)
* ThyParse.token list)) list
-end;
+ end;
signature THY_SYN =
-sig
+ sig
val parse: string -> string -> string
-end;
+ end;
-functor ThySynFun(ThySynData: THY_SYN_DATA): THY_SYN =
+functor ThySynFun (Data: THY_SYN_DATA): THY_SYN =
struct
-open ThyParse ThySynData;
+val syntax =
+ ThyParse.make_syntax (ThyParse.pure_keywords @ Data.user_keywords)
+ (ThyParse.pure_sections @ Data.user_sections);
-val syntax =
- make_syntax (pure_keywords @ user_keywords) (pure_sections @ user_sections);
-
-val parse = parse_thy syntax;
+val parse = ThyParse.parse_thy syntax;
end;