src/Pure/ML/ml_env.ML
changeset 62875 5a0c06491974
parent 62873 2f9c8a18f832
child 62876 507c90523113
equal deleted inserted replaced
62874:b0194643e64c 62875:5a0c06491974
    99       val sml_tables' =
    99       val sml_tables' =
   100         sml_tables |> (fn (val1, type1, fixity1, structure1, signature1, functor1) =>
   100         sml_tables |> (fn (val1, type1, fixity1, structure1, signature1, functor1) =>
   101             let
   101             let
   102               val val2 =
   102               val val2 =
   103                 fold (fn (x, y) =>
   103                 fold (fn (x, y) =>
   104                   member (op =) ML_Name_Space.excluded_values x ? Symtab.update (x, y))
   104                   member (op =) ML_Name_Space.bootstrap_values x ? Symtab.update (x, y))
   105                 (#allVal ML_Name_Space.global ()) val1;
   105                 (#allVal ML_Name_Space.global ()) val1;
   106               val structure2 =
   106               val structure2 =
   107                 fold (fn (x, y) =>
   107                 fold (fn (x, y) =>
   108                   member (op =) ML_Name_Space.excluded_structures x ? Symtab.update (x, y))
   108                   member (op =) ML_Name_Space.bootstrap_structures x ? Symtab.update (x, y))
   109                 (#allStruct ML_Name_Space.global ()) structure1;
   109                 (#allStruct ML_Name_Space.global ()) structure1;
   110             in (val2, type1, fixity1, structure2, signature1, functor1) end);
   110             in (val2, type1, fixity1, structure2, signature1, functor1) end);
   111     in make_data (bootstrap, tables, sml_tables', breakpoints) end);
   111     in make_data (bootstrap, tables, sml_tables', breakpoints) end);
   112 
   112 
   113 fun add_name_space {SML} (space: ML_Name_Space.T) =
   113 fun add_name_space {SML} (space: ML_Name_Space.T) =