--- a/src/HOL/Tools/function_package/mutual.ML Tue Apr 10 11:12:42 2007 +0200
+++ b/src/HOL/Tools/function_package/mutual.ML Tue Apr 10 11:12:55 2007 +0200
@@ -209,19 +209,8 @@
end
-(* Beta-reduce both sides of a meta-equality *)
-fun beta_norm_eq thm =
- let
- val (lhs, rhs) = dest_equals (cprop_of thm)
- val lhs_conv = beta_conversion false lhs
- val rhs_conv = beta_conversion false rhs
- in
- transitive (symmetric lhs_conv) (transitive thm rhs_conv)
- end
-
fun beta_reduce thm = Thm.equal_elim (Thm.beta_conversion true (cprop_of thm)) thm
-
fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F =
let
val thy = ProofContext.theory_of ctxt