--- a/Quot/Nominal/nominal_permeq.ML	Wed Feb 24 17:32:43 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,71 +0,0 @@
-(*  Title:      nominal_thmdecls.ML
-    Author:     Brian Huffman, Christian Urban
-*)
-
-signature NOMINAL_PERMEQ =
-sig
-  val eqvt_tac: Proof.context -> int -> tactic 
-
-end;
-
-(* TODO:
-
- - provide a method interface with the usual add and del options
-
- - print a warning if for a constant no eqvt lemma is stored
-
- - there seems to be too much simplified in case of multiple 
-   permutations, like
-
-      p o q o r o x 
-
-   we usually only want the outermost permutation to "float" in
-*)
-
-
-structure Nominal_Permeq: NOMINAL_PERMEQ =
-struct
-
-local
-
-fun eqvt_apply_conv ctxt ct =
-  case (term_of ct) of
-    (Const (@{const_name "permute"}, _) $ _ $ (_ $ _)) =>
-      let
-        val (perm, t) = Thm.dest_comb ct
-        val (_, p) = Thm.dest_comb perm
-        val (f, x) = Thm.dest_comb t
-        val a = ctyp_of_term x;
-        val b = ctyp_of_term t;
-        val ty_insts = map SOME [b, a]
-        val term_insts = map SOME [p, f, x]
-      in
-        Drule.instantiate' ty_insts term_insts @{thm eqvt_apply}
-      end
-  | _ => Conv.no_conv ct
-
-fun eqvt_lambda_conv ctxt ct =
-  case (term_of ct) of
-    (Const (@{const_name "permute"}, _) $ _ $ Abs _) =>
-      Conv.rewr_conv @{thm eqvt_lambda} ct
-  | _ => Conv.no_conv ct
-
-in
-
-fun eqvt_conv ctxt ct =
-  Conv.first_conv
-    [ Conv.rewr_conv @{thm eqvt_bound},
-      eqvt_apply_conv ctxt
-        then_conv Conv.comb_conv (eqvt_conv ctxt),
-      eqvt_lambda_conv ctxt
-        then_conv Conv.abs_conv (fn (v, ctxt) => eqvt_conv ctxt) ctxt,
-      More_Conv.rewrs_conv (Nominal_ThmDecls.get_eqvts_raw_thms ctxt),
-      Conv.all_conv
-    ] ct
-
-fun eqvt_tac ctxt = 
-  CONVERSION (More_Conv.bottom_conv (fn ctxt => eqvt_conv ctxt) ctxt)
-
-end
-
-end; (* structure *)
\ No newline at end of file