--- a/src/ZF/Tools/induct_tacs.ML Thu Sep 15 17:16:55 2005 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Thu Sep 15 17:16:56 2005 +0200
@@ -70,7 +70,7 @@
struct
fun datatype_info thy name =
- (case Symtab.curried_lookup (DatatypesData.get thy) name of
+ (case Symtab.lookup (DatatypesData.get thy) name of
SOME info => info
| NONE => error ("Unknown datatype " ^ quote name));
@@ -166,8 +166,8 @@
thy
|> Theory.add_path (Sign.base_name big_rec_name)
|> (#1 o PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])])
- |> DatatypesData.put (Symtab.curried_update (big_rec_name, dt_info) (DatatypesData.get thy))
- |> ConstructorsData.put (fold_rev Symtab.curried_update con_pairs (ConstructorsData.get thy))
+ |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
+ |> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
|> Theory.parent_path
end;