make SML/NJ more happy;
authorwenzelm
Thu Apr 09 22:53:26 2015 +0200 (2015-04-09)
changeset 59992d8db5172c23f
parent 59991 09be0495dcc2
child 59993 8f6cacc87f42
make SML/NJ more happy;
src/Doc/Isar_Ref/Proof.thy
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Probability/measurable.ML
src/HOL/ROOT
     1.1 --- a/src/Doc/Isar_Ref/Proof.thy	Thu Apr 09 20:42:38 2015 +0200
     1.2 +++ b/src/Doc/Isar_Ref/Proof.thy	Thu Apr 09 22:53:26 2015 +0200
     1.3 @@ -565,7 +565,7 @@
     1.4    that method @{text m\<^sub>1} is applied with restriction to the first subgoal,
     1.5    then @{text m\<^sub>2} is applied consecutively with restriction to each subgoal
     1.6    that has newly emerged due to @{text m\<^sub>1}. This is analogous to the tactic
     1.7 -  combinator @{ML THEN_ALL_NEW} in Isabelle/ML, see also @{cite
     1.8 +  combinator @{ML_op THEN_ALL_NEW} in Isabelle/ML, see also @{cite
     1.9    "isabelle-implementation"}. For example, @{text "(rule r; blast)"} applies
    1.10    rule @{text "r"} and then solves all new subgoals by @{text blast}.
    1.11  
     2.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Thu Apr 09 20:42:38 2015 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Thu Apr 09 22:53:26 2015 +0200
     2.3 @@ -162,7 +162,7 @@
     2.4  fun fresh_star_const T U =
     2.5    Const (@{const_name Nominal.fresh_star}, HOLogic.mk_setT T --> U --> HOLogic.boolT);
     2.6  
     2.7 -fun gen_nominal_datatype prep_specs config dts thy =
     2.8 +fun gen_nominal_datatype prep_specs (config: Old_Datatype_Aux.config) dts thy =
     2.9    let
    2.10      val new_type_names = map (fn ((tname, _, _), _) => Binding.name_of tname) dts;
    2.11  
     3.1 --- a/src/HOL/Probability/measurable.ML	Thu Apr 09 20:42:38 2015 +0200
     3.2 +++ b/src/HOL/Probability/measurable.ML	Thu Apr 09 22:53:26 2015 +0200
     3.3 @@ -51,14 +51,14 @@
     3.4      dest_thms : thm Item_Net.T,
     3.5      cong_thms : thm Item_Net.T,
     3.6      preprocessors : (string * preprocessor) list }
     3.7 -  val empty = {
     3.8 +  val empty: T = {
     3.9      measurable_thms = Item_Net.init eq_measurable_thms (single o Thm.prop_of o fst),
    3.10      dest_thms = Thm.full_rules,
    3.11      cong_thms = Thm.full_rules,
    3.12      preprocessors = [] };
    3.13    val extend = I;
    3.14    fun merge ({measurable_thms = t1, dest_thms = dt1, cong_thms = ct1, preprocessors = i1 },
    3.15 -      {measurable_thms = t2, dest_thms = dt2, cong_thms = ct2, preprocessors = i2 }) = {
    3.16 +      {measurable_thms = t2, dest_thms = dt2, cong_thms = ct2, preprocessors = i2 }) : T = {
    3.17      measurable_thms = Item_Net.merge (t1, t2),
    3.18      dest_thms = Item_Net.merge (dt1, dt2),
    3.19      cong_thms = Item_Net.merge (ct1, ct2),
    3.20 @@ -81,7 +81,7 @@
    3.21  fun map_cong_thms f = map_data I I f I
    3.22  fun map_preprocessors f = map_data I I I f
    3.23  
    3.24 -fun generic_add_del map = 
    3.25 +fun generic_add_del map : attribute context_parser =
    3.26    Scan.lift
    3.27      (Args.add >> K Item_Net.update || Args.del >> K Item_Net.remove || Scan.succeed Item_Net.update) >>
    3.28      (fn f => Thm.declaration_attribute (Data.map o map o f))
     4.1 --- a/src/HOL/ROOT	Thu Apr 09 20:42:38 2015 +0200
     4.2 +++ b/src/HOL/ROOT	Thu Apr 09 22:53:26 2015 +0200
     4.3 @@ -229,7 +229,7 @@
     4.4    document_files "root.bib" "root.tex"
     4.5  
     4.6  session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
     4.7 -  options [document = false, browser_info = false]
     4.8 +  options [condition = ML_SYSTEM_POLYML, document = false, browser_info = false]
     4.9    theories
    4.10      Generate
    4.11      Generate_Binary_Nat
    4.12 @@ -673,7 +673,7 @@
    4.13  
    4.14      TPTP-related extensions.
    4.15    *}
    4.16 -  options [document = false]
    4.17 +  options [condition = ML_SYSTEM_POLYML, document = false]
    4.18    theories
    4.19      ATP_Theory_Export
    4.20      MaSh_Eval