diff -r 3885dc2669f9 -r abafea9b39bb Nominal/nominal_dt_rawfuns.ML
--- a/Nominal/nominal_dt_rawfuns.ML	Thu Aug 26 02:08:00 2010 +0800
+++ b/Nominal/nominal_dt_rawfuns.ML	Fri Aug 27 02:03:52 2010 +0800
@@ -62,6 +62,9 @@
 datatype bmode = Lst | Res | Set
 datatype bclause = BC of bmode * (term option * int) list * int list
 
+fun lookup xs x = the (AList.lookup (op=) xs x)
+
+
 (* testing for concrete atom types *)
 fun is_atom ctxt ty =
   Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base})
@@ -166,7 +169,9 @@
   in
     case bn_option of
       NONE => (setify lthy arg, @{term "{}::atom set"})
-    | SOME bn => (to_set (bn $ arg), the (AList.lookup (op=) fv_bn_map bn) $ arg)
+    | SOME bn => (to_set (bn $ arg), 
+       if  member (op=) bodies i then @{term "{}::atom set"}  
+       else lookup fv_bn_map bn $ arg)
   end  
 
   val t1 = map (mk_fv_body fv_map args) bodies
@@ -189,7 +194,7 @@
                  NONE => mk_supp arg
                | SOME fv => fv $ arg)
     | SOME (NONE) => @{term "{}::atom set"}
-    | SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg
+    | SOME (SOME bn) => lookup fv_bn_map bn $ arg
   end  
 in
   case bclause of
@@ -201,7 +206,7 @@
 let
   val arg_names = Datatype_Prop.make_tnames arg_tys
   val args = map Free (arg_names ~~ arg_tys)
-  val fv = the (AList.lookup (op=) fv_map ty)
+  val fv = lookup fv_map ty
   val lhs = fv $ list_comb (constr, args)
   val rhs_trms = map (mk_fv_rhs lthy fv_map fv_bn_map args) bclauses
   val rhs = fold_union rhs_trms
@@ -213,7 +218,7 @@
 let
   val arg_names = Datatype_Prop.make_tnames arg_tys
   val args = map Free (arg_names ~~ arg_tys)
-  val fv_bn = the (AList.lookup (op=) fv_bn_map bn_trm)
+  val fv_bn = lookup fv_bn_map bn_trm
   val lhs = fv_bn $ list_comb (constr, args)
   val rhs_trms = map (mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args) bclauses
   val rhs = fold_union rhs_trms