src/Pure/Thy/thy_parse.ML
changeset 1512 ce37c64244c0
parent 1383 be42217b0b5c
child 1539 f21c8fab7c3c
--- a/src/Pure/Thy/thy_parse.ML	Fri Feb 16 17:24:51 1996 +0100
+++ b/src/Pure/Thy/thy_parse.ML	Fri Feb 16 18:00:47 1996 +0100
@@ -10,7 +10,7 @@
 infix 0 ||;
 
 signature THY_PARSE =
-sig
+  sig
   type token
   val !! : ('a -> 'b * 'c) -> 'a -> 'b * 'c
   val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
@@ -66,9 +66,10 @@
   val mk_pair: string * string -> string
   val mk_triple: string * string * string -> string
   val strip_quotes: string -> string
-end;
+  end;
 
-functor ThyParseFun(structure Symtab: SYMTAB and ThyScan: THY_SCAN): THY_PARSE=
+
+structure ThyParse : THY_PARSE=
 struct
 
 open ThyScan;
@@ -517,5 +518,4 @@
   axm_section "axclass" "|> AxClass.add_axclass" axclass_decl,
   section "instance" "" instance_decl];
 
-
 end;