changeset 76670 | b04d45bebbc5 |
parent 68918 | 3a0db30e5d87 |
child 78728 | 72631efa3821 |
--- a/src/Pure/ML_Bootstrap.thy Sat Dec 17 19:09:46 2022 +0100 +++ b/src/Pure/ML_Bootstrap.thy Sat Dec 17 19:19:10 2022 +0100 @@ -8,8 +8,6 @@ imports Pure begin -external_file "$POLYML_EXE" - ML \<open> #allStruct ML_Name_Space.global () |> List.app (fn (name, _) => if member (op =) ML_Name_Space.hidden_structures name then