I have just done a fetch and can no longer build Isabelle/HOL. I hope somebody can fix this soon. Larry
Building HOL ... HOL FAILED (see also /Users/lp15/.isabelle/heaps//polyml-5.2.1_x86-darwin/log/HOL) *** Warning: Pattern is not exhaustive. Found near *** val ( [ isom_def], cdef_thy) = |>( |>( ...), ...(...)) (line 140 of "/Users/lp15/isabelle/Repos/src/HOL/Tools/record.ML") *** structure IsTupleSupport : *** sig *** val add_istuple_type : *** bstring * string list -> *** Term.typ * Term.typ -> *** Context.theory -> Term.term * Term.term * Context.theory *** val dest_cons_tuple : Term.term -> Term.term * Term.term *** val istuple_intros_tac : Context.theory -> int -> Tactical.tactic *** val mk_cons_tuple : Term.term * Term.term -> Term.term *** val named_cterm_instantiate : *** (string * Thm.cterm) list -> Thm.thm -> Thm.thm *** end *** Error: Mixed right and left associative operators of the same precedence. (line 2124 of "/Users/lp15/isabelle/Repos/src/HOL/Tools/ record.ML") *** Error: Mixed right and left associative operators of the same precedence. (line 2128 of "/Users/lp15/isabelle/Repos/src/HOL/Tools/ record.ML") *** Exception- Fail "Static errors (pass 1)" raised *** At command "use" (line 459 of "/Users/lp15/isabelle/Repos/src/HOL/ Record.thy"). Exception- TOPLEVEL_ERROR raised *** ML error make: *** [/Users/lp15/.isabelle/heaps//polyml-5.2.1_x86-darwin/HOL] Error 1 ~/isabelle/Repos/src/HOL:
