# HG changeset patch
# User urbanc
# Date 1141038876 -3600
# Node ID 9c8793c62d0c63f4278ea18db1ba95c540d6790a
# Parent  a64fef2d7073ae7de1c25038e166678a88beb897
added support for arbitrary atoms in the simproc

diff -r a64fef2d7073 -r 9c8793c62d0c src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Sun Feb 26 23:01:50 2006 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML	Mon Feb 27 12:14:36 2006 +0100
@@ -15,33 +15,30 @@
 fun perm_eval_tac ss i =
     let
         val perm_eq_app   = thm "nominal.pt_fun_app_eq";
-        val at_inst       = dynamic_thm ss "at_name_inst";
-        val pt_inst       = dynamic_thm ss "pt_name_inst";
 
         fun perm_eval_simproc sg ss redex =
         (case redex of 
         (* case pi o (f x) == (pi o f) (pi o x)    *)
         (* special treatment in cases of constants *)
-        (Const("nominal.perm",Type("fun",[Type("List.list",[Type("*",[ty,_])]),_])) $ pi $ (f $ x)) 
-        => let
-             val _ = warning ("type: "^Sign.string_of_typ (sign_of (the_context())) ty)
+        (Const("nominal.perm",
+           Type("fun",[Type("List.list",[Type("*",[Type(n,_),_])]),_])) $ pi $ (f $ x)) => 
+           let
+             val name = Sign.base_name n
+             val at_inst = dynamic_thm ss ("at_"^name^"_inst");
+             val pt_inst = dynamic_thm ss ("pt_"^name^"_inst");
            in
 
-           (case f of
+           (case (head_of f) of
                     (* nothing to do on constants *)
-                    (* FIXME: proper treatment of constants *)
-                      Const(_,_)                   => NONE
-                    | (Const(_,_) $ _)             => NONE
-                    | ((Const(_,_) $ _) $ _)       => NONE
-                    | (((Const(_,_) $ _) $ _) $ _) => NONE
+                      Const _ => NONE
                     | _ => 
                        (* FIXME: analyse type here or at "pty"*)
 		       SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection))
             end
 
         (* case pi o (%x. f x) == (%x. pi o (f ((rev pi)o x))) *)
-        | (Const("nominal.perm",_) $ pi $ (Abs _)) 
-        => let 
+        | (Const("nominal.perm",_) $ pi $ (Abs _)) => 
+           let 
              val perm_fun_def = thm "nominal.perm_fun_def"
            in SOME (perm_fun_def) end