equal
deleted
inserted
replaced
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 (Long_Name.base_name big_rec_name) |
160 |> Sign.add_path (Long_Name.base_name big_rec_name) |
161 |> PureThy.add_thmss [((Binding.name "simps", simps), [Simplifier.simp_add])] |> snd |
161 |> Global_Theory.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; |
166 |
166 |