Datatype.ML

--- a/Datatype.ML	Tue Mar 22 18:07:45 1994 +0100
+++ b/Datatype.ML	Tue Mar 22 19:54:55 1994 +0100
@@ -11,6 +11,7 @@
    val inject : thm list
    val ineq : thm list 
    val cases : thm list
+   val simps : thm list
    val induct_tac : string -> int -> tactic
 end;
 
@@ -480,6 +481,8 @@
 
 val cases = getaxioms rules_case thy;
 
+val simps = inject @ ineq @ cases;
+
 fun induct_tac a = res_inst_tac [(datatype_id,a)] induct;
 
 (* -------------------------------------------------------------------  *)