src/Pure/Thy/thy_parse.ML
changeset 1810 0eef167ebe1b
parent 1705 19fe0ab646b4
child 1850 c6b6ccfd390c
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Mon Jun 17 16:51:47 1996 +0200
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Tue Jun 18 16:17:38 1996 +0200
     1.3 @@ -311,12 +311,15 @@
     1.4    optional ("(" $$-- !! (name --$$ ")")) "\"logic\"" -- string >> mk_pair;
     1.5  
     1.6  val trans_arrow =
     1.7 -  $$ "=>" >> K " |-> " ||
     1.8 -  $$ "<=" >> K " <-| " ||
     1.9 -  $$ "==" >> K " <-> ";
    1.10 +  $$ "=>" >> K "Syntax.|-> " ||
    1.11 +  $$ "<=" >> K "Syntax.<-| " ||
    1.12 +  $$ "==" >> K "Syntax.<-> ";
    1.13  
    1.14 -val trans_decls = repeat1 (trans_pat ^^ !! (trans_arrow ^^ trans_pat))
    1.15 -  >> mk_big_list;
    1.16 +val trans_line =
    1.17 +    trans_pat -- !! (trans_arrow -- trans_pat) >>
    1.18 +        (fn (left, (arr, right)) => arr ^ "(" ^ left ^ ",\t" ^ right ^ ")");
    1.19 +
    1.20 +val trans_decls = repeat1 trans_line >> mk_big_list;
    1.21  
    1.22  
    1.23  (* ML translations *)