src/Pure/ML/ml_thms.ML
author wenzelm
Fri, 17 Jul 2020 15:08:56 +0200
changeset 72284 6c75287276d5
parent 70680 41108e3e9ca5
permissions -rw-r--r--
tuned -- avoid non-standard extend/merge;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML/ml_thms.ML
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
     3
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
     4
Attribute source and theorem values within ML.
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
     5
*)
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
     6
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
     7
signature ML_THMS =
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
     8
sig
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 56304
diff changeset
     9
  val the_attributes: Proof.context -> int -> Token.src list
48782
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    10
  val the_thmss: Proof.context -> thm list list
56199
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
    11
  val get_stored_thms: unit -> thm list
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
    12
  val get_stored_thm: unit -> thm
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
    13
  val store_thms: string * thm list -> unit
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
    14
  val store_thm: string * thm -> unit
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
    15
  val bind_thm: string * thm -> unit
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
    16
  val bind_thms: string * thm list -> unit
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    17
end;
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    18
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    19
structure ML_Thms: ML_THMS =
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    20
struct
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    21
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    22
(* auxiliary data *)
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    23
48782
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    24
type thms = (string * bool) * thm list;  (*name, single, value*)
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    25
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    26
structure Data = Proof_Data
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    27
(
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 56304
diff changeset
    28
  type T = Token.src list Inttab.table * thms list;
48782
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    29
  fun init _ = (Inttab.empty, []);
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    30
);
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    31
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    32
val put_attributes = Data.map o apfst o Inttab.update;
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    33
fun the_attributes ctxt name = the (Inttab.lookup (fst (Data.get ctxt)) name);
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    34
48782
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    35
val get_thmss = snd o Data.get;
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    36
val the_thmss = map snd o get_thmss;
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    37
val cons_thms = Data.map o apsnd o cons;
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    38
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    39
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    40
(* attribute source *)
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    41
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53169
diff changeset
    42
val _ = Theory.setup
67147
dea94b1aabc3 prefer control symbol antiquotations;
wenzelm
parents: 66067
diff changeset
    43
  (ML_Antiquotation.declaration \<^binding>\<open>attributes\<close> Attrib.attribs
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 59127
diff changeset
    44
    (fn _ => fn srcs => fn ctxt =>
59112
e670969f34df expand ML cartouches to Input.source;
wenzelm
parents: 58866
diff changeset
    45
      let val i = serial () in
e670969f34df expand ML cartouches to Input.source;
wenzelm
parents: 58866
diff changeset
    46
        ctxt
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 59127
diff changeset
    47
        |> put_attributes (i, srcs)
59112
e670969f34df expand ML cartouches to Input.source;
wenzelm
parents: 58866
diff changeset
    48
        |> ML_Context.value_decl "attributes"
e670969f34df expand ML cartouches to Input.source;
wenzelm
parents: 58866
diff changeset
    49
            ("ML_Thms.the_attributes ML_context " ^ string_of_int i)
e670969f34df expand ML cartouches to Input.source;
wenzelm
parents: 58866
diff changeset
    50
      end));
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    51
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    52
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    53
(* fact references *)
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    54
56069
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    55
fun thm_binding kind is_single thms ctxt =
48782
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    56
  let
53169
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    57
    val initial = null (get_thmss ctxt);
59112
e670969f34df expand ML cartouches to Input.source;
wenzelm
parents: 58866
diff changeset
    58
    val (name, ctxt') = ML_Context.variant kind ctxt;
53169
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    59
    val ctxt'' = cons_thms ((name, is_single), thms) ctxt';
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    60
59127
723b11f8ffbf more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents: 59112
diff changeset
    61
    val ml_body = ML_Context.struct_name ctxt ^ "." ^ name;
53169
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    62
    fun decl final_ctxt =
48782
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    63
      if initial then
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    64
        let
53169
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    65
          val binds = get_thmss final_ctxt |> map (fn ((a, b), _) => (b ? enclose "[" "]") a);
48782
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    66
          val ml_env = "val [" ^ commas binds ^ "] = ML_Thms.the_thmss ML_context;\n";
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    67
        in (ml_env, ml_body) end
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    68
      else ("", ml_body);
56069
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    69
  in (decl, ctxt'') end;
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    70
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53169
diff changeset
    71
val _ = Theory.setup
67147
dea94b1aabc3 prefer control symbol antiquotations;
wenzelm
parents: 66067
diff changeset
    72
  (ML_Antiquotation.declaration \<^binding>\<open>thm\<close> (Attrib.thm >> single) (K (thm_binding "thm" true)) #>
dea94b1aabc3 prefer control symbol antiquotations;
wenzelm
parents: 66067
diff changeset
    73
   ML_Antiquotation.declaration \<^binding>\<open>thms\<close> Attrib.thms (K (thm_binding "thms" false)));
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    74
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    75
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    76
(* ad-hoc goals *)
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    77
30266
970bf4f594c9 ML antiquotation @{lemma}: allow 'and' list, proper simultaneous type-checking;
wenzelm
parents: 29606
diff changeset
    78
val and_ = Args.$$$ "and";
58866
f81e11391562 clarified syntax -- avoid overlap with command category;
wenzelm
parents: 58045
diff changeset
    79
val by = Parse.reserved "by";
63121
629a4c5e953e embedded content may be delimited via cartouches;
wenzelm
parents: 62900
diff changeset
    80
val goal = Scan.unless (by || and_) Args.embedded_inner_syntax;
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    81
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53169
diff changeset
    82
val _ = Theory.setup
67147
dea94b1aabc3 prefer control symbol antiquotations;
wenzelm
parents: 66067
diff changeset
    83
  (ML_Antiquotation.declaration \<^binding>\<open>lemma\<close>
56069
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    84
    (Scan.lift (Args.mode "open" -- Parse.enum1 "and" (Scan.repeat1 goal) --
58866
f81e11391562 clarified syntax -- avoid overlap with command category;
wenzelm
parents: 58045
diff changeset
    85
      (Parse.position by -- Method.parse -- Scan.option Method.parse)))
f81e11391562 clarified syntax -- avoid overlap with command category;
wenzelm
parents: 58045
diff changeset
    86
    (fn _ => fn ((is_open, raw_propss), (((_, by_pos), m1), m2)) => fn ctxt =>
56069
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    87
      let
66067
cdbcb417db67 more markup for HTML rendering;
wenzelm
parents: 63121
diff changeset
    88
        val reports =
cdbcb417db67 more markup for HTML rendering;
wenzelm
parents: 63121
diff changeset
    89
          (by_pos, Markup.keyword1 |> Markup.keyword_properties) ::
cdbcb417db67 more markup for HTML rendering;
wenzelm
parents: 63121
diff changeset
    90
            maps Method.reports_of (m1 :: the_list m2);
58866
f81e11391562 clarified syntax -- avoid overlap with command category;
wenzelm
parents: 58045
diff changeset
    91
        val _ = Context_Position.reports ctxt reports;
55515
0e161deca64d more markup;
wenzelm
parents: 55111
diff changeset
    92
56069
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    93
        val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
70680
41108e3e9ca5 formal position for PThm nodes;
wenzelm
parents: 67715
diff changeset
    94
        val prep_result = Goal.norm_result ctxt #> not is_open ? Thm.close_derivation \<^here>;
56069
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    95
        fun after_qed res goal_ctxt =
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    96
          Proof_Context.put_thms false (Auto_Bind.thisN,
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    97
            SOME (map prep_result (Proof_Context.export goal_ctxt ctxt (flat res)))) goal_ctxt;
53169
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    98
56069
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    99
        val ctxt' = ctxt
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
   100
          |> Proof.theorem NONE after_qed propss
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
   101
          |> Proof.global_terminal_proof (m1, m2);
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
   102
        val thms =
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
   103
          Proof_Context.get_fact ctxt'
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
   104
            (Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN)));
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
   105
      in thm_binding "lemma" (length (flat propss) = 1) thms ctxt end));
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
   106
56199
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   107
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   108
(* old-style theorem bindings *)
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   109
72284
6c75287276d5 tuned -- avoid non-standard extend/merge;
wenzelm
parents: 70680
diff changeset
   110
structure Data = Theory_Data
56199
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   111
(
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   112
  type T = thm list;
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   113
  val empty = [];
72284
6c75287276d5 tuned -- avoid non-standard extend/merge;
wenzelm
parents: 70680
diff changeset
   114
  val extend = I;
6c75287276d5 tuned -- avoid non-standard extend/merge;
wenzelm
parents: 70680
diff changeset
   115
  val merge = #1;
56199
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   116
);
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   117
72284
6c75287276d5 tuned -- avoid non-standard extend/merge;
wenzelm
parents: 70680
diff changeset
   118
fun get_stored_thms () = Data.get (Context.the_global_context ());
56199
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   119
val get_stored_thm = hd o get_stored_thms;
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   120
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   121
fun ml_store get (name, ths) =
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   122
  let
67715
ec46ecb87999 tuned signature;
wenzelm
parents: 67147
diff changeset
   123
    val (_, ths') =
ec46ecb87999 tuned signature;
wenzelm
parents: 67147
diff changeset
   124
      Context.>>> (Context.map_theory_result
ec46ecb87999 tuned signature;
wenzelm
parents: 67147
diff changeset
   125
        (Global_Theory.note_thms "" ((Binding.name name, []), [(ths, [])])));
72284
6c75287276d5 tuned -- avoid non-standard extend/merge;
wenzelm
parents: 70680
diff changeset
   126
    val _ = Theory.setup (Data.put ths');
56199
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   127
    val _ =
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   128
      if name = "" then ()
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   129
      else if not (ML_Syntax.is_identifier name) then
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   130
        error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value")
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   131
      else
56304
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56275
diff changeset
   132
        ML_Compiler.eval (ML_Compiler.verbose true ML_Compiler.flags) Position.none
56199
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   133
          (ML_Lex.tokenize ("val " ^ name ^ " = " ^ get ^ " ();"));
72284
6c75287276d5 tuned -- avoid non-standard extend/merge;
wenzelm
parents: 70680
diff changeset
   134
    val _ = Theory.setup (Data.put []);
56199
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   135
  in () end;
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   136
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   137
val store_thms = ml_store "ML_Thms.get_stored_thms";
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   138
fun store_thm (name, th) = ml_store "ML_Thms.get_stored_thm" (name, [th]);
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   139
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   140
fun bind_thm (name, thm) = store_thm (name, Drule.export_without_context thm);
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   141
fun bind_thms (name, thms) = store_thms (name, map Drule.export_without_context thms);
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   142
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
   143
end;