[isabelle-dev] compilation of IsarRef is broken

[Ondřej Kunčar]

Hi!
It seems that the compilation of IsarRef is broken. I've got the 
following error with the 45669:06e259492f6b changeset:

~/tmp/isabelle-dev/doc-src/IsarRef> ../../bin/isabelle make
Running HOL-IsarRef ...
HOL-IsarRef FAILED

   val CONTEXT_REWRITE_RULE :
      term * term list * thm * thm list -> thm -> thm * term list
   val CONJUNCTS : thm -> thm list val CONJUNCT2 : thm -> thm
   val CONJUNCT1 : thm -> thm val CHOOSE : cterm * thm -> thm -> thm
   val ASSUME : cterm -> thm end

Loading theory "Misc"
### Introduced fixed type variable(s): 'a in "B" or "x__"
### Introduced fixed type variable(s): 'a in "a"
### Introduced fixed type variable(s): 'a in "A" or "x__"
### Introduced fixed type variable(s): 'a in "A"
### Introduced fixed type variable(s): 'a in "A" or "x__"
*** Theory loader: failed to load "HOL_Specific" (unresolved "Old_Recdef")
*** Error (line 786 of "~~/src/HOL/Tools/TFL/rules.ML"):
*** Value or constructor (add_eqcong) has not been declared in structure 
Simplifier
***
*** At command "use" (line 70 of "~~/src/HOL/Library/Old_Recdef.thy")
val it = (): unit
Exception- TOPLEVEL_ERROR raised
*** ML error

make: *** 
[~/.isabelle//heaps/polyml-5.4.0_x86_64-linux/log/HOL-IsarRef.gz] Error 1

Any ideas what's wrong?

Ondrej