src/ZF/Tools/induct_tacs.ML
changeset 6970 ac37a8fcaad1
parent 6851 526c0b90bcef
child 8438 b8389b4fca9c
equal deleted inserted replaced
6969:441393b452c7 6970:ac37a8fcaad1
   181 	       ((big_rec_name, dt_info), DatatypesData.get thy)) 
   181 	       ((big_rec_name, dt_info), DatatypesData.get thy)) 
   182 	  |> ConstructorsData.put
   182 	  |> ConstructorsData.put
   183 	       (foldr Symtab.update (con_pairs, ConstructorsData.get thy))
   183 	       (foldr Symtab.update (con_pairs, ConstructorsData.get thy))
   184 	  |> Theory.parent_path
   184 	  |> Theory.parent_path
   185   end
   185   end
   186   handle _ => error "Failure in rep_datatype";
   186   handle exn => (writeln "Failure in rep_datatype"; raise exn);
   187 
   187 
   188 end;
   188 end;
   189 
   189 
   190 
   190 
   191 val exhaust_tac = DatatypeTactics.exhaust_tac;
   191 val exhaust_tac = DatatypeTactics.exhaust_tac;