TFL/casesplit.ML

      Seq.hd o (ALLGOALS (fn i => REPEAT (etac Drule.thin_rl i)));
 
 (* get the case_thm (my version) from a type *)
 fun case_thm_of_ty sgn ty  = 
     let 
-      val dtypestab = DatatypePackage.get_datatypes_sg sgn;
+      val dtypestab = DatatypePackage.get_datatypes sgn;
       val ty_str = case ty of 
                      Type(ty_str, _) => ty_str
                    | TFree(s,_)  => raise ERROR_MESSAGE 
                                             ("Free type: " ^ s)   
                    | TVar((s,i),_) => raise ERROR_MESSAGE