src/Pure/pure.ML
changeset 5211 c02b0c727780
parent 5092 e443bc494604
child 5247 4a8e6e60bbf8
     1.1 --- a/src/Pure/pure.ML	Tue Jul 28 17:05:34 1998 +0200
     1.2 +++ b/src/Pure/pure.ML	Wed Jul 29 15:38:08 1998 +0200
     1.3 @@ -2,26 +2,27 @@
     1.4      ID:         $Id$
     1.5      Author:     Markus Wenzel, TU Muenchen
     1.6  
     1.7 -The actual Pure and CPure theories.
     1.8 +Setup the actual Pure and CPure theories.
     1.9  *)
    1.10  
    1.11  structure Pure =
    1.12  struct
    1.13 -
    1.14 -val thy =
    1.15 -  PureThy.begin_theory "Pure" [ProtoPure.thy]
    1.16 -  |> Theory.add_syntax Syntax.pure_appl_syntax
    1.17 -  |> PureThy.end_theory;
    1.18 -
    1.19 +  val thy =
    1.20 +    PureThy.begin_theory "Pure" [ProtoPure.thy]
    1.21 +    |> Theory.add_syntax Syntax.pure_appl_syntax
    1.22 +    |> PureThy.end_theory;
    1.23  end;
    1.24  
    1.25 -
    1.26  structure CPure =
    1.27  struct
    1.28 +  val thy =
    1.29 +    PureThy.begin_theory "CPure" [ProtoPure.thy]
    1.30 +    |> Theory.add_syntax Syntax.pure_applC_syntax
    1.31 +    |> PureThy.end_theory;
    1.32 +end;
    1.33  
    1.34 -val thy =
    1.35 -  PureThy.begin_theory "CPure" [ProtoPure.thy]
    1.36 -  |> Theory.add_syntax Syntax.pure_applC_syntax
    1.37 -  |> PureThy.end_theory;
    1.38 -
    1.39 -end;
    1.40 +ThyInfo.loaded_thys :=
    1.41 +  (Symtab.make (map ThyInfo.mk_info
    1.42 +    [("ProtoPure", ["Pure", "CPure"], [], ProtoPure.thy),
    1.43 +     ("Pure", [], ["ProtoPure"], Pure.thy),
    1.44 +     ("CPure", [], ["ProtoPure"], CPure.thy)]));