# HG changeset patch
# User wenzelm
# Date 877601455 -7200
# Node ID d3c2159b75fad2d2dfd8d26fe7ecfcfc70c40457
# Parent  1be726ef681327ed8f721f4b4bbd4c395effb628
Sign.stamp_names_of;

diff -r 1be726ef6813 -r d3c2159b75fa src/Pure/goals.ML
--- a/src/Pure/goals.ML	Thu Oct 23 12:10:32 1997 +0200
+++ b/src/Pure/goals.ML	Thu Oct 23 12:10:55 1997 +0200
@@ -111,11 +111,10 @@
 
 (*Generates the list of new theories when the proof state's signature changes*)
 fun sign_error (sign,sign') =
-  let val stamps = #stamps(Sign.rep_sg sign') \\ 
-                   #stamps(Sign.rep_sg sign)
-  in  case stamps of
-        [stamp] => "\nNew theory: " ^ !stamp
-      | _       => "\nNew theories: " ^ space_implode ", " (map ! stamps)
+  let val names = Sign.stamp_names_of sign' \\ Sign.stamp_names_of sign
+  in  case names of
+        [name] => "\nNew theory: " ^ name
+      | _       => "\nNew theories: " ^ space_implode ", " names
   end;
 
 (*Default action is to print an error message; could be suppressed for
diff -r 1be726ef6813 -r d3c2159b75fa src/Pure/section_utils.ML
--- a/src/Pure/section_utils.ML	Thu Oct 23 12:10:32 1997 +0200
+++ b/src/Pure/section_utils.ML	Thu Oct 23 12:10:55 1997 +0200
@@ -66,5 +66,5 @@
 
 (*Check for some named theory*)
 fun require_thy thy name sect =
-  if exists (equal name o !) (stamps_of_thy thy) then ()
+  if exists (equal name) (Sign.stamp_names_of (sign_of thy)) then ()
   else error ("Need theory " ^ quote name ^ " as an ancestor for " ^ sect);