# HG changeset patch
# User narboux
# Date 1173713139 -3600
# Node ID b3526cd2a3368d8e3eefdf04fd10f4e09ee4c96f
# Parent  c9e384a956df722b67101ec257d673286856cf93
removes some unused code that used to try to derive a simpler version of the eqvt lemmas

diff -r c9e384a956df -r b3526cd2a336 src/HOL/Nominal/nominal_thmdecls.ML
--- a/src/HOL/Nominal/nominal_thmdecls.ML	Mon Mar 12 11:07:59 2007 +0100
+++ b/src/HOL/Nominal/nominal_thmdecls.ML	Mon Mar 12 16:25:39 2007 +0100
@@ -153,26 +153,6 @@
     | _ => raise EQVT_FORM "All permutation should be the same")
   end;
 
-fun tactic_eqvt_simple_form thy orig_thm = 
-  let val perm_pi_simp = dynamic_thms thy "perm_pi_simp"
-      val _ = (warning "perm_pi_simp :";map print_thm perm_pi_simp)
-  in
-   tactic ("Try to prove simple eqvt form.",
-    asm_full_simp_tac (HOL_basic_ss addsimps [perm_fun_def,orig_thm]@perm_pi_simp) 1)
-  end
-
-fun derive_simple_statement thy oldlhs orig_thm pi typi typrm =
-let val goal_term =
-  case (strip_comb oldlhs) of   
-    (Const (f,t),args) =>  
-       let val lhs = Const ("Nominal.perm",Type ("fun",[typi,Type ("fun",[t,t])])) $ Var(pi,typi) $ Const (f,t)
-       in  Logic.unvarify (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,Const(f,t)))) end
-   | _ => raise EQVT_FORM "Error deriving simple version."
-  val _ = Display.print_cterm (cterm_of thy goal_term)  
-in
-  Goal.prove_global thy [] [] goal_term (fn _ =>  tactic_eqvt_simple_form thy orig_thm)
-end
-
 (* Either adds a theorem (orig_thm) to or deletes one from the equivaraince *)
 (* lemma list depending on flag. To be added the lemma has to satisfy a     *)
 (* certain form. *) 
@@ -194,15 +174,9 @@
        (* case: eqvt-lemma is of the equational form *)  
       | (Const ("Trueprop", _) $ (Const ("op =", _) $ 
             (Const ("Nominal.perm",typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
-	   let val optth = ([derive_simple_statement thy lhs orig_thm pi typi typrm] 
-		handle (ERROR s) => (warning ("Couldn't prove the simple version:\n"^s);[])
-			| _ => (warning "Couldn't prove the simple version";[])
-		)
-	    in
 	   (if (apply_pi lhs (pi,typi)) = rhs 
-               then orig_thm::optth   
+               then [orig_thm]
                else raise EQVT_FORM "Type Equality")
-	   end
       | _ => raise EQVT_FORM "Type unknown")
   in 
       update_context flag thms_to_be_added context