--- a/src/HOL/Tools/res_clause.ML Thu Sep 15 17:16:55 2005 +0200
+++ b/src/HOL/Tools/res_clause.ML Thu Sep 15 17:16:56 2005 +0200
@@ -141,12 +141,12 @@
fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
fun make_fixed_const c =
- case Symtab.curried_lookup const_trans_table c of
+ case Symtab.lookup const_trans_table c of
SOME c' => c'
| NONE => const_prefix ^ ascii_of c;
fun make_fixed_type_const c =
- case Symtab.curried_lookup type_const_trans_table c of
+ case Symtab.lookup type_const_trans_table c of
SOME c' => c'
| NONE => tconst_prefix ^ ascii_of c;