src/Pure/Syntax/syntax.ML
changeset 9372 7834e56e2277
parent 8894 0281bde335ca
child 10454 9ef2f60ebde5
     1.1 --- a/src/Pure/Syntax/syntax.ML	Sun Jul 16 20:59:31 2000 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Sun Jul 16 21:00:10 2000 +0200
     1.3 @@ -141,13 +141,7 @@
     1.4  type ruletab = (Ast.ast * Ast.ast) list Symtab.table;
     1.5  
     1.6  fun dest_ruletab tab = flat (map snd (Symtab.dest tab));
     1.7 -
     1.8 -
     1.9 -(* lookup_ruletab *)
    1.10 -
    1.11 -fun lookup_ruletab tab =
    1.12 -  if Symtab.is_empty tab then None
    1.13 -  else Some (fn a => Symtab.lookup_multi (tab, a));
    1.14 +fun lookup_ruletab tab a = Symtab.lookup_multi (tab, a);
    1.15  
    1.16  
    1.17  (* empty, extend, merge ruletabs *)