# HG changeset patch
# User wenzelm
# Date 979846617 -3600
# Node ID ef2b1dd40db99f5c02852524d25900dacafde6fb
# Parent  7c7a7b0e1d0cd61d59428f445f664d60702acefe
use Sign.PureN, Sign.CPureN;

diff -r 7c7a7b0e1d0c -r ef2b1dd40db9 src/Pure/pure.ML
--- a/src/Pure/pure.ML	Thu Jan 18 20:36:31 2001 +0100
+++ b/src/Pure/pure.ML	Thu Jan 18 20:36:57 2001 +0100
@@ -23,7 +23,7 @@
   structure Pure =
   struct
     val thy =
-      PureThy.begin_theory "Pure" [ProtoPure.thy]
+      PureThy.begin_theory Sign.PureN [ProtoPure.thy]
       |> Theory.add_syntax Syntax.pure_appl_syntax
       |> Library.apply common_setup
       |> PureThy.end_theory;
@@ -32,7 +32,7 @@
   structure CPure =
   struct
     val thy =
-      PureThy.begin_theory "CPure" [ProtoPure.thy]
+      PureThy.begin_theory Sign.CPureN [ProtoPure.thy]
       |> Theory.add_syntax Syntax.pure_applC_syntax
       |> Library.apply common_setup
       |> Theory.copy