src/ZF/Tools/induct_tacs.ML
changeset 30280 eb98b49ef835
parent 29579 cb520b766e00
child 30364 577edc39b501
equal deleted inserted replaced
30279:84097bba7bdc 30280:eb98b49ef835
   155     (*associate with each constructor the datatype name and rewrites*)
   155     (*associate with each constructor the datatype name and rewrites*)
   156     val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors
   156     val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors
   157 
   157 
   158   in
   158   in
   159     thy
   159     thy
   160     |> Sign.add_path (Sign.base_name big_rec_name)
   160     |> Sign.add_path (NameSpace.base_name big_rec_name)
   161     |> PureThy.add_thmss [((Binding.name "simps", simps), [Simplifier.simp_add])] |> snd
   161     |> PureThy.add_thmss [((Binding.name "simps", simps), [Simplifier.simp_add])] |> snd
   162     |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
   162     |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
   163     |> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
   163     |> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
   164     |> Sign.parent_path
   164     |> Sign.parent_path
   165   end;
   165   end;