--- a/Nominal-General/nominal_thmdecls.ML	Fri Apr 09 09:02:54 2010 -0700
+++ b/Nominal-General/nominal_thmdecls.ML	Fri Apr 09 21:51:01 2010 +0200
@@ -60,7 +60,18 @@
 val add_thm = EqvtData.map o Item_Net.update;
 val del_thm = EqvtData.map o Item_Net.remove;
 
-val add_raw_thm = EqvtRawData.map o Item_Net.update;
+fun is_equiv (Const ("==", _) $ _ $ _) = true
+  | is_equiv _ = false
+
+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
+end
+
 val del_raw_thm = EqvtRawData.map o Item_Net.remove;
 
 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
@@ -78,7 +89,7 @@
    rtac (thm RS @{thm trans}),
    rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}]
 
-(* transform equations into the required form *)
+(* transform equations into the "p o c = c"-form *)
 fun transform_eq ctxt thm lhs rhs = 
 let
   val (p, t) = dest_perm lhs