src/Pure/Thy/thy_parse.ML

 infix 5 -- --$$ $$-- ^^;
 infix 3 >>;
 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
   val || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b
   val -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e

   val mk_list: string list -> string
   val mk_big_list: string list -> string
   val mk_pair: string * string -> string
   val mk_triple: string * string * string -> string
   val strip_quotes: string -> string
-end;
-
-functor ThyParseFun(structure Symtab: SYMTAB and ThyScan: THY_SCAN): THY_PARSE=
+  end;
+
+
+structure ThyParse : THY_PARSE=
 struct
 
 open ThyScan;
 
 

   axm_section "rules" "|> add_axioms" axiom_decls,
   axm_section "defs" "|> add_defs" axiom_decls,
   axm_section "axclass" "|> AxClass.add_axclass" axclass_decl,
   section "instance" "" instance_decl];
 
-
 end;