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