--- a/src/ZF/Tools/induct_tacs.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Mon Sep 20 16:05:25 2010 +0200
@@ -158,7 +158,7 @@
in
thy
|> Sign.add_path (Long_Name.base_name big_rec_name)
- |> PureThy.add_thmss [((Binding.name "simps", simps), [Simplifier.simp_add])] |> snd
+ |> Global_Theory.add_thmss [((Binding.name "simps", simps), [Simplifier.simp_add])] |> snd
|> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
|> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
|> Sign.parent_path