equal
deleted
inserted
replaced
180 seq (writeln o Sign.string_of_term sign o #2) axpairs |
180 seq (writeln o Sign.string_of_term sign o #2) axpairs |
181 else () |
181 else () |
182 |
182 |
183 (*add definitions of the inductive sets*) |
183 (*add definitions of the inductive sets*) |
184 val thy1 = thy |> Theory.add_path big_rec_base_name |
184 val thy1 = thy |> Theory.add_path big_rec_base_name |
185 |> (#1 o PureThy.add_defs_i (map Thm.no_attributes axpairs)) |
185 |> (#1 o PureThy.add_defs_i false (map Thm.no_attributes axpairs)) |
186 |
186 |
187 |
187 |
188 (*fetch fp definitions from the theory*) |
188 (*fetch fp definitions from the theory*) |
189 val big_rec_def::part_rec_defs = |
189 val big_rec_def::part_rec_defs = |
190 map (get_def thy1) |
190 map (get_def thy1) |