# HG changeset patch
# User krauss
# Date 1176196375 -7200
# Node ID c9e3de6dd8c2898c3a9754dad7d9ac7e91e80b76
# Parent  166b4c3b41c0e99c2769908b21e542aefc8cb873
removed dead code

diff -r 166b4c3b41c0 -r c9e3de6dd8c2 src/HOL/Tools/function_package/mutual.ML
--- 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