--- a/Nominal-General/nominal_thmdecls.ML	Sun Apr 11 22:47:45 2010 +0200
+++ b/Nominal-General/nominal_thmdecls.ML	Sun Apr 11 22:48:49 2010 +0200
@@ -38,6 +38,8 @@
 structure Nominal_ThmDecls: NOMINAL_THMDECLS =
 struct
 
+fun mk_equiv r = r RS @{thm eq_reflection};
+fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;
 
 structure EqvtData = Generic_Data
 ( type T = thm Item_Net.T;
@@ -66,16 +68,16 @@
 fun add_raw_thm thm = 
 let
   val trm = prop_of thm
-  val _ = if is_equiv trm then () 
-    else raise THM ("Theorem must be a meta-equality", 0, [thm]) 
 in
-  (EqvtRawData.map o Item_Net.update) thm
+  if is_equiv trm 
+  then (EqvtRawData.map o Item_Net.update) thm
+  else raise THM ("Theorem must be a meta-equality", 0, [thm]) 
 end
 
 val del_raw_thm = EqvtRawData.map o Item_Net.remove;
 
 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
-  | dest_perm t = raise TERM("dest_perm", [t])
+  | dest_perm t = raise TERM ("dest_perm", [t])
 
 fun mk_perm p trm =
 let
@@ -90,11 +92,12 @@
    rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}]
 
 (* transform equations into the "p o c = c"-form *)
-fun transform_eq ctxt thm lhs rhs = 
+fun transform_eq ctxt thm = 
 let
+  val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))
   val (p, t) = dest_perm lhs
   val (c, args) = strip_comb t
-  val (c', args') = strip_comb rhs 
+  val (c', args') = strip_comb rhs
   val eargs = map Envir.eta_contract args 
   val eargs' = map Envir.eta_contract args'
   val p_str = fst (fst (dest_Var p))
@@ -113,15 +116,12 @@
 fun transform addel_fun thm context = 
 let
   val ctxt = Context.proof_of context
-  val trm = HOLogic.dest_Trueprop (prop_of thm)
 in
-  case trm of
-    Const (@{const_name "op ="}, _) $ lhs $ rhs =>
-      let 
-        val thm' = transform_eq ctxt thm lhs rhs RS @{thm eq_reflection}
-      in
-        addel_fun thm' context
-      end
+  case (prop_of thm) of
+    @{const "Trueprop"} $ (Const (@{const_name "op ="}, _) $ _ $ _) =>
+      addel_fun (safe_mk_equiv (transform_eq ctxt thm)) context
+  | @{const "==>"} $ _ $ _ => 
+      error ("not yet implemented")
   | _ => raise (error "only (op=) case implemented yet")
 end