--- a/src/HOL/Tools/Function/fun_cases.ML Fri Mar 06 14:01:08 2015 +0100
+++ b/src/HOL/Tools/Function/fun_cases.ML Fri Mar 06 15:58:56 2015 +0100
@@ -29,7 +29,7 @@
val info = Function.get_info ctxt f handle List.Empty => err ();
val {elims, pelims, is_partial, ...} = info;
val elims = if is_partial then pelims else the elims;
- val cprop = Proof_Context.cterm_of ctxt prop;
+ val cprop = Thm.cterm_of ctxt prop;
fun mk_elim rl =
Thm.implies_intr cprop
(Tactic.rule_by_tactic ctxt (Inductive.mk_cases_tac ctxt) (Thm.assume cprop RS rl))