src/Pure/pure.ML
changeset 5863 9935800edf58
parent 5839 3ad1364bbb4b
child 5905 68cdba6c178f
equal deleted inserted replaced
5862:3a1f9ec7c8a2 5863:9935800edf58
    26   struct
    26   struct
    27     val thy =
    27     val thy =
    28       PureThy.begin_theory "CPure" [ProtoPure.thy]
    28       PureThy.begin_theory "CPure" [ProtoPure.thy]
    29       |> Theory.add_syntax Syntax.pure_applC_syntax
    29       |> Theory.add_syntax Syntax.pure_applC_syntax
    30       |> Theory.apply common_setup
    30       |> Theory.apply common_setup
    31       |> Theory.prep_ext                  (*copy shared data!*)
    31       |> Theory.copy
    32       |> PureThy.end_theory;
    32       |> PureThy.end_theory;
    33   end;
    33   end;
    34 end;
    34 end;
    35 
    35 
    36 ThyInfo.loaded_thys :=
    36 ThyInfo.loaded_thys :=