--- 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}.
--- 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;
--- 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))
--- 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