src/Pure/Thy/thy_parse.ML
changeset 3958 78a8e9a1c2f9
parent 3931 c3c287d3f502
child 3977 9b3cbfd6a936
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Mon Oct 20 15:20:42 1997 +0200
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Mon Oct 20 17:08:18 1997 +0200
     1.3 @@ -415,7 +415,7 @@
     1.4  
     1.5  (* local, global path *)
     1.6  
     1.7 -val empty_decl = empty >> K "";
     1.8 +fun empty_decl toks = (empty >> K "") toks;
     1.9  
    1.10  val global_path =
    1.11    "|> (fn thy => if ! global_names then thy else Theory.add_path \"/\" thy)";