use Sign.PureN, Sign.CPureN;
authorwenzelm
Thu, 18 Jan 2001 20:36:57 +0100
changeset 10931 ef2b1dd40db9
parent 10930 7c7a7b0e1d0c
child 10932 ad13abb0a264
use Sign.PureN, Sign.CPureN;
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