src/ZF/Tools/induct_tacs.ML
changeset 24712 64ed05609568
parent 22846 fb79144af9a3
child 24725 04b676d1a1fe
     1.1 --- a/src/ZF/Tools/induct_tacs.ML	Tue Sep 25 15:34:35 2007 +0200
     1.2 +++ b/src/ZF/Tools/induct_tacs.ML	Tue Sep 25 17:06:14 2007 +0200
     1.3 @@ -157,11 +157,11 @@
     1.4  
     1.5    in
     1.6      thy
     1.7 -    |> Theory.add_path (Sign.base_name big_rec_name)
     1.8 +    |> Sign.add_path (Sign.base_name big_rec_name)
     1.9      |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add])] |> snd
    1.10      |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
    1.11      |> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
    1.12 -    |> Theory.parent_path
    1.13 +    |> Sign.parent_path
    1.14    end;
    1.15  
    1.16  fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =