src/HOL/Main.ML

- Expressed infer_derivs' in terms of infer_deriv
- Eta-expanded function instantiate to delay evaluation (avoids inefficiencies
when proof terms are switched off)

structure Main =
struct
  val thy = the_context ();
end;