--- a/Admin/jenkins/run_build Mon Oct 08 15:42:43 2018 +0200
+++ b/Admin/jenkins/run_build Mon Oct 08 17:12:28 2018 +0200
@@ -10,4 +10,5 @@
bin/isabelle components -a
bin/isabelle jedit -bf
+bin/isabelle ocaml_setup
bin/isabelle "ci_build_$PROFILE" "$@"
--- a/src/Pure/name.ML Mon Oct 08 15:42:43 2018 +0200
+++ b/src/Pure/name.ML Mon Oct 08 17:12:28 2018 +0200
@@ -151,9 +151,9 @@
(* names conforming to typical requirements of identifiers in the world outside *)
-fun enforce_case' false cs =
+fun enforce_case' false cs =
(if forall Symbol.is_ascii_upper cs then map else nth_map 0) Symbol.to_ascii_lower cs
- | enforce_case' true cs =
+ | enforce_case' true cs =
nth_map 0 Symbol.to_ascii_upper cs;
fun enforce_case upper = implode o enforce_case' upper o raw_explode;
--- a/src/Pure/raw_simplifier.ML Mon Oct 08 15:42:43 2018 +0200
+++ b/src/Pure/raw_simplifier.ML Mon Oct 08 17:12:28 2018 +0200
@@ -569,7 +569,7 @@
val Simpset (_, {mk_rews = {mk, ...}, ...}) = simpset_of ctxt;
val mk =
if sym then fn ctxt => fn th => (mk ctxt th) RL [Drule.symmetric_thm]
- else mk
+ else mk
in maps (fn thm => map (rpair (Thm.get_name_hint thm)) (mk ctxt thm)) thms
end;