Isar setups;
authorwenzelm
Mon Nov 09 15:41:24 1998 +0100 (1998-11-09)
changeset 58393ad1364bbb4b
parent 5838 a4122945d638
child 5840 e2d2b896c717
Isar setups;
src/Pure/pure.ML
     1.1 --- a/src/Pure/pure.ML	Mon Nov 09 15:40:26 1998 +0100
     1.2 +++ b/src/Pure/pure.ML	Mon Nov 09 15:41:24 1998 +0100
     1.3 @@ -5,22 +5,32 @@
     1.4  Setup the actual Pure and CPure theories.
     1.5  *)
     1.6  
     1.7 -structure Pure =
     1.8 -struct
     1.9 -  val thy =
    1.10 -    PureThy.begin_theory "Pure" [ProtoPure.thy]
    1.11 -    |> Theory.add_syntax Syntax.pure_appl_syntax
    1.12 -    |> Theory.apply Locale.setup
    1.13 -    |> PureThy.end_theory;
    1.14 -end;
    1.15 +local
    1.16 +  val common_setup =
    1.17 +    ObjectLogic.setup @
    1.18 +    Locale.setup @
    1.19 +    ProofContext.setup @
    1.20 +    Method.setup @
    1.21 +    Attrib.setup;
    1.22 +in
    1.23 +  structure Pure =
    1.24 +  struct
    1.25 +    val thy =
    1.26 +      PureThy.begin_theory "Pure" [ProtoPure.thy]
    1.27 +      |> Theory.add_syntax Syntax.pure_appl_syntax
    1.28 +      |> Theory.apply common_setup
    1.29 +      |> PureThy.end_theory;
    1.30 +  end;
    1.31  
    1.32 -structure CPure =
    1.33 -struct
    1.34 -  val thy =
    1.35 -    PureThy.begin_theory "CPure" [ProtoPure.thy]
    1.36 -    |> Theory.add_syntax Syntax.pure_applC_syntax
    1.37 -    |> Theory.apply Locale.setup
    1.38 -    |> PureThy.end_theory;
    1.39 +  structure CPure =
    1.40 +  struct
    1.41 +    val thy =
    1.42 +      PureThy.begin_theory "CPure" [ProtoPure.thy]
    1.43 +      |> Theory.add_syntax Syntax.pure_applC_syntax
    1.44 +      |> Theory.apply common_setup
    1.45 +      |> Theory.prep_ext                  (*copy shared data!*)
    1.46 +      |> PureThy.end_theory;
    1.47 +  end;
    1.48  end;
    1.49  
    1.50  ThyInfo.loaded_thys :=