src/Pure/Syntax/syntax.ML

--- a/src/Pure/Syntax/syntax.ML	Sun Jul 16 20:59:31 2000 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sun Jul 16 21:00:10 2000 +0200
@@ -141,13 +141,7 @@
 type ruletab = (Ast.ast * Ast.ast) list Symtab.table;
 
 fun dest_ruletab tab = flat (map snd (Symtab.dest tab));
-
-
-(* lookup_ruletab *)
-
-fun lookup_ruletab tab =
-  if Symtab.is_empty tab then None
-  else Some (fn a => Symtab.lookup_multi (tab, a));
+fun lookup_ruletab tab a = Symtab.lookup_multi (tab, a);
 
 
 (* empty, extend, merge ruletabs *)