# HG changeset patch
# User berghofe
# Date 1155547570 -7200
# Node ID 3baf326b2b5f759da5820baf921f583e3ac5905c
# Parent  53b31f7c1d8770da24621fcb07d4dcf13e3e2934
Removed non-trivial definitions from calc_atm theorem list.

diff -r 53b31f7c1d87 -r 3baf326b2b5f src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Mon Aug 14 11:25:08 2006 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Mon Aug 14 11:26:10 2006 +0200
@@ -770,7 +770,9 @@
 		  val thms2 = inst_dj [at_fresh_ineq]
 	      in [(("fresh_atm", thms1 @ thms2),[])] end
             ||>> PureThy.add_thmss
-	      let val thms1 = List.concat (List.concat perm_defs)
+	      let val thms1 = filter
+                (fn th => case prop_of th of _ $ _ $ Var _ => true | _ => false)
+                (List.concat (List.concat perm_defs))
               in [(("calc_atm", (inst_at at_calc) @ thms1),[])] end
             ||>> PureThy.add_thmss
 	      let val thms1 = inst_pt_at [abs_fun_pi]