(* Title:  fixed type for _RE_parsing of strings from frontend 

    Author: Walther Neuper

    9911xx 

    (c) due to copyright terms

    with hints from Markus Wenzel

  *)

 theory Typefix imports "../ProgLang/Script" begin

 syntax

   "_plus"  :: 'a

   "_minus" :: 'a

   "_umin"  :: 'a

   "_times" :: 'a

 translations

   "op +"  => "_plus  :: [real, real]  => real"  (*infixl 65    *)

   "op -"  => "_minus :: [real, real] => real"   (*infixl 65    *)

   "uminus"=> "_umin  :: [real] => real"         (*"- _" [80] 80*)

   "op *"  => "_times :: [real, real] => real"   (*infixl 70    *)

 ML {*

 val parse_translation = 

     [("_plus", curry Term.list_comb (Syntax.const "op +")),  

      ("_minus", curry Term.list_comb (Syntax.const "op -")), 

      ("_umin", curry Term.list_comb (Syntax.const "uminus")),

      ("_times", curry Term.list_comb (Syntax.const "op *"))];

 *}

 end