src/Pure/Syntax/syntax.ML
changeset 9372 7834e56e2277
parent 8894 0281bde335ca
child 10454 9ef2f60ebde5
equal deleted inserted replaced
9371:2f06293f291a 9372:7834e56e2277
   139 (** tables of translation rules **)
   139 (** tables of translation rules **)
   140 
   140 
   141 type ruletab = (Ast.ast * Ast.ast) list Symtab.table;
   141 type ruletab = (Ast.ast * Ast.ast) list Symtab.table;
   142 
   142 
   143 fun dest_ruletab tab = flat (map snd (Symtab.dest tab));
   143 fun dest_ruletab tab = flat (map snd (Symtab.dest tab));
   144 
   144 fun lookup_ruletab tab a = Symtab.lookup_multi (tab, a);
   145 
       
   146 (* lookup_ruletab *)
       
   147 
       
   148 fun lookup_ruletab tab =
       
   149   if Symtab.is_empty tab then None
       
   150   else Some (fn a => Symtab.lookup_multi (tab, a));
       
   151 
   145 
   152 
   146 
   153 (* empty, extend, merge ruletabs *)
   147 (* empty, extend, merge ruletabs *)
   154 
   148 
   155 fun extend_ruletab tab rules =
   149 fun extend_ruletab tab rules =