# HG changeset patch
# User paulson
# Date 863693670 -7200
# Node ID 16b840e02899bc0c89afbb682cc22cb7994bbc72
# Parent  c522bc46aea78653aeb497c90ce427571130cb5a
Improved error message in "require_thy"

diff -r c522bc46aea7 -r 16b840e02899 src/HOL/datatype.ML
--- a/src/HOL/datatype.ML	Thu May 15 12:54:02 1997 +0200
+++ b/src/HOL/datatype.ML	Thu May 15 12:54:30 1997 +0200
@@ -139,7 +139,7 @@
   fun add_datatype (typevars, tname, cons_list') thy = 
     let
       val dummy = if length cons_list' < dtK then ()
-                  else require_thy thy "Nat" "datatype";
+                  else require_thy thy "Nat" "datatype definitions";
       
       fun typid(dtRek(_,id)) = id
         | typid(dtVar s) = implode (tl (explode s))