# HG changeset patch # User wenzelm # Date 918056816 -3600 # Node ID 381b27ca05439572a7613ff7b349a432c0b5bce5 # Parent f0c14e527d68240d0b9719c4626b618435b7b308 renamed sig to PRIVATE_SIGN; diff -r f0c14e527d68 -r 381b27ca0543 src/Pure/sign.ML --- a/src/Pure/sign.ML Wed Feb 03 16:46:31 1999 +0100 +++ b/src/Pure/sign.ML Wed Feb 03 16:46:56 1999 +0100 @@ -130,7 +130,7 @@ val class_of_const: string -> class end; -signature SIGN_PRIVATE = +signature PRIVATE_SIGN = sig include SIGN val init_data: Object.kind * (Object.T * (Object.T -> Object.T) * @@ -140,7 +140,7 @@ val print_data: Object.kind -> sg -> unit end; -structure Sign: SIGN_PRIVATE = +structure Sign: PRIVATE_SIGN = struct