src/ZF/Tools/induct_tacs.ML
changeset 6970 ac37a8fcaad1
parent 6851 526c0b90bcef
child 8438 b8389b4fca9c
--- a/src/ZF/Tools/induct_tacs.ML	Sat Jul 10 21:50:49 1999 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Sat Jul 10 21:51:25 1999 +0200
@@ -183,7 +183,7 @@
 	       (foldr Symtab.update (con_pairs, ConstructorsData.get thy))
 	  |> Theory.parent_path
   end
-  handle _ => error "Failure in rep_datatype";
+  handle exn => (writeln "Failure in rep_datatype"; raise exn);
 
 end;