--- a/src/HOL/Tools/Function/function_elims.ML Mon Sep 16 17:04:28 2013 +0200
+++ b/src/HOL/Tools/Function/function_elims.ML Mon Sep 16 17:13:38 2013 +0200
@@ -14,7 +14,7 @@
signature FUNCTION_ELIMS =
sig
val dest_funprop : term -> (term * term list) * term
- val mk_partial_elim_rules : local_theory ->
+ val mk_partial_elim_rules : Proof.context ->
Function_Common.function_result -> thm list list
end;
@@ -74,8 +74,11 @@
in
-fun mk_partial_elim_rules ctxt result=
- let val FunctionResult {fs, G, R, dom, psimps, simple_pinducts, cases,
+fun mk_partial_elim_rules ctxt result =
+ let
+ val thy = Proof_Context.theory_of ctxt;
+
+ val FunctionResult {fs, G, R, dom, psimps, simple_pinducts, cases,
termination, domintros, ...} = result;
val n_fs = length fs;
@@ -105,7 +108,6 @@
val sumtree_inj = SumTree.mk_inj domT n_fs (idx+1) args;
- val thy = Proof_Context.theory_of ctxt;
val cprop = cterm_of thy prop
val asms = [cprop, cterm_of thy (HOLogic.mk_Trueprop (dom $ sumtree_inj))];