| changeset 26474 | 94735cff132c |
| parent 26380 | 5d368eb42c11 |
| child 28151 | 61f9c918b410 |
--- a/src/Pure/ML-Systems/polyml_common.ML Fri Mar 28 22:39:45 2008 +0100 +++ b/src/Pure/ML-Systems/polyml_common.ML Fri Mar 28 22:39:47 2008 +0100 @@ -15,6 +15,9 @@ (** ML system and platform related **) +val forget_structure = PolyML.Compiler.forgetStructure; + + (* Compiler options *) val ml_system_fix_ints = false;