# HG changeset patch
# User wenzelm
# Date 1428612806 -7200
# Node ID d8db5172c23f6dfdfcf5a02751891be61aa2cfe2
# Parent  09be0495dcc2015aea497ca978d59bbd1e672822
make SML/NJ more happy;

diff -r 09be0495dcc2 -r d8db5172c23f src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Thu Apr 09 20:42:38 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy	Thu Apr 09 22:53:26 2015 +0200
@@ -565,7 +565,7 @@
   that method @{text m\<^sub>1} is applied with restriction to the first subgoal,
   then @{text m\<^sub>2} is applied consecutively with restriction to each subgoal
   that has newly emerged due to @{text m\<^sub>1}. This is analogous to the tactic
-  combinator @{ML THEN_ALL_NEW} in Isabelle/ML, see also @{cite
+  combinator @{ML_op THEN_ALL_NEW} in Isabelle/ML, see also @{cite
   "isabelle-implementation"}. For example, @{text "(rule r; blast)"} applies
   rule @{text "r"} and then solves all new subgoals by @{text blast}.
 
diff -r 09be0495dcc2 -r d8db5172c23f src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Thu Apr 09 20:42:38 2015 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Thu Apr 09 22:53:26 2015 +0200
@@ -162,7 +162,7 @@
 fun fresh_star_const T U =
   Const (@{const_name Nominal.fresh_star}, HOLogic.mk_setT T --> U --> HOLogic.boolT);
 
-fun gen_nominal_datatype prep_specs config dts thy =
+fun gen_nominal_datatype prep_specs (config: Old_Datatype_Aux.config) dts thy =
   let
     val new_type_names = map (fn ((tname, _, _), _) => Binding.name_of tname) dts;
 
diff -r 09be0495dcc2 -r d8db5172c23f src/HOL/Probability/measurable.ML
--- a/src/HOL/Probability/measurable.ML	Thu Apr 09 20:42:38 2015 +0200
+++ b/src/HOL/Probability/measurable.ML	Thu Apr 09 22:53:26 2015 +0200
@@ -51,14 +51,14 @@
     dest_thms : thm Item_Net.T,
     cong_thms : thm Item_Net.T,
     preprocessors : (string * preprocessor) list }
-  val empty = {
+  val empty: T = {
     measurable_thms = Item_Net.init eq_measurable_thms (single o Thm.prop_of o fst),
     dest_thms = Thm.full_rules,
     cong_thms = Thm.full_rules,
     preprocessors = [] };
   val extend = I;
   fun merge ({measurable_thms = t1, dest_thms = dt1, cong_thms = ct1, preprocessors = i1 },
-      {measurable_thms = t2, dest_thms = dt2, cong_thms = ct2, preprocessors = i2 }) = {
+      {measurable_thms = t2, dest_thms = dt2, cong_thms = ct2, preprocessors = i2 }) : T = {
     measurable_thms = Item_Net.merge (t1, t2),
     dest_thms = Item_Net.merge (dt1, dt2),
     cong_thms = Item_Net.merge (ct1, ct2),
@@ -81,7 +81,7 @@
 fun map_cong_thms f = map_data I I f I
 fun map_preprocessors f = map_data I I I f
 
-fun generic_add_del map = 
+fun generic_add_del map : attribute context_parser =
   Scan.lift
     (Args.add >> K Item_Net.update || Args.del >> K Item_Net.remove || Scan.succeed Item_Net.update) >>
     (fn f => Thm.declaration_attribute (Data.map o map o f))
diff -r 09be0495dcc2 -r d8db5172c23f src/HOL/ROOT
--- a/src/HOL/ROOT	Thu Apr 09 20:42:38 2015 +0200
+++ b/src/HOL/ROOT	Thu Apr 09 22:53:26 2015 +0200
@@ -229,7 +229,7 @@
   document_files "root.bib" "root.tex"
 
 session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
-  options [document = false, browser_info = false]
+  options [condition = ML_SYSTEM_POLYML, document = false, browser_info = false]
   theories
     Generate
     Generate_Binary_Nat
@@ -673,7 +673,7 @@
 
     TPTP-related extensions.
   *}
-  options [document = false]
+  options [condition = ML_SYSTEM_POLYML, document = false]
   theories
     ATP_Theory_Export
     MaSh_Eval