src/Pure/Syntax/extension.ML
changeset 117 6b26ccac50fc
parent 116 fdc1c3424247
child 166 79e61c182b22
equal deleted inserted replaced
116:fdc1c3424247 117:6b26ccac50fc
   231 
   231 
   232 fun extend_xgram (XGram xgram) (Ext ext, SynRules rules) =
   232 fun extend_xgram (XGram xgram) (Ext ext, SynRules rules) =
   233   let
   233   let
   234     fun descend (from, to) = Mfix ("_", to --> from, "", [0], 0);
   234     fun descend (from, to) = Mfix ("_", to --> from, "", [0], 0);
   235 
   235 
   236     fun parents T = Mfix ("(1'(_'))", T --> T, "", [0], max_pri);
   236     fun parents T = Mfix ("'(_')", T --> T, "", [0], max_pri);
   237 
   237 
   238     fun mkappl T =
   238     fun mkappl T =
   239       Mfix ("(1_/(1'(_')))", [funT, argsT] ---> T, applC, [max_pri, 0], max_pri);
   239       Mfix ("(1_/(1'(_')))", [funT, argsT] ---> T, applC, [max_pri, 0], max_pri);
   240 
   240 
   241     fun mkid T = Mfix ("_", idT --> T, "", [], max_pri);
   241     fun mkid T = Mfix ("_", idT --> T, "", [], max_pri);