--- a/src/HOL/Codatatype/Tools/bnf_gfp_util.ML Tue Sep 04 17:23:08 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp_util.ML Tue Sep 04 18:14:58 2012 +0200
@@ -35,9 +35,6 @@
val mk_undefined: typ -> term
val mk_univ: term -> term
- val mk_sum_case: term -> term -> term
- val mk_sum_caseN: term list -> term
-
val mk_specN: int -> thm -> thm
val mk_sum_casesN: int -> int -> thm
@@ -182,18 +179,6 @@
A $ f1 $ f2 $ b1 $ b2
end;
-fun mk_sum_case f g =
- let
- val fT = fastype_of f;
- val gT = fastype_of g;
- in
- Const (@{const_name sum_case},
- fT --> gT --> mk_sumT (domain_type fT, domain_type gT) --> range_type fT) $ f $ g
- end;
-
-fun mk_sum_caseN [f] = f
- | mk_sum_caseN (f :: fs) = mk_sum_case f (mk_sum_caseN fs);
-
fun mk_InN_not_InM 1 _ = @{thm Inl_not_Inr}
| mk_InN_not_InM n m =
if n > m then mk_InN_not_InM m n RS @{thm not_sym}