# HG changeset patch
# User wenzelm
# Date 910622484 -3600
# Node ID 3ad1364bbb4b56e33efa53c580db9c4eb174b69f
# Parent  a4122945d638efdc21c7c174a7ceb30b173e0273
Isar setups;

diff -r a4122945d638 -r 3ad1364bbb4b src/Pure/pure.ML
--- a/src/Pure/pure.ML	Mon Nov 09 15:40:26 1998 +0100
+++ b/src/Pure/pure.ML	Mon Nov 09 15:41:24 1998 +0100
@@ -5,22 +5,32 @@
 Setup the actual Pure and CPure theories.
 *)
 
-structure Pure =
-struct
-  val thy =
-    PureThy.begin_theory "Pure" [ProtoPure.thy]
-    |> Theory.add_syntax Syntax.pure_appl_syntax
-    |> Theory.apply Locale.setup
-    |> PureThy.end_theory;
-end;
+local
+  val common_setup =
+    ObjectLogic.setup @
+    Locale.setup @
+    ProofContext.setup @
+    Method.setup @
+    Attrib.setup;
+in
+  structure Pure =
+  struct
+    val thy =
+      PureThy.begin_theory "Pure" [ProtoPure.thy]
+      |> Theory.add_syntax Syntax.pure_appl_syntax
+      |> Theory.apply common_setup
+      |> PureThy.end_theory;
+  end;
 
-structure CPure =
-struct
-  val thy =
-    PureThy.begin_theory "CPure" [ProtoPure.thy]
-    |> Theory.add_syntax Syntax.pure_applC_syntax
-    |> Theory.apply Locale.setup
-    |> PureThy.end_theory;
+  structure CPure =
+  struct
+    val thy =
+      PureThy.begin_theory "CPure" [ProtoPure.thy]
+      |> Theory.add_syntax Syntax.pure_applC_syntax
+      |> Theory.apply common_setup
+      |> Theory.prep_ext                  (*copy shared data!*)
+      |> PureThy.end_theory;
+  end;
 end;
 
 ThyInfo.loaded_thys :=