--- a/Nominal/nominal_dt_rawfuns.ML	Thu May 27 18:40:10 2010 +0200
+++ b/Nominal/nominal_dt_rawfuns.ML	Mon May 31 19:57:29 2010 +0200
@@ -21,12 +21,11 @@
   val mk_atom_set: term -> term
   val mk_atom_fset: term -> term
 
-
   val setify: Proof.context -> term -> term
   val listify: Proof.context -> term -> term
 
   val define_raw_fvs: Datatype_Aux.descr -> (string * sort) list -> bn_info ->
-    bclause list list list -> Proof.context -> term list * term list * thm list * local_theory
+    bclause list list list -> thm list -> Proof.context -> term list * term list * thm list * local_theory
 end
 
 
@@ -200,7 +199,7 @@
   map2 (mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess
 end
 
-fun define_raw_fvs descr sorts bn_info bclausesss lthy =
+fun define_raw_fvs descr sorts bn_info bclausesss constr_thms lthy =
 let
   val fv_names = prefix_dt_names descr sorts "fv_"
   val fv_arg_tys = all_dtyps descr sorts
@@ -224,16 +223,8 @@
   val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
   val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs)
 
-  fun pat_completeness_auto lthy =
-    Pat_Completeness.pat_completeness_tac lthy 1
-      THEN auto_tac (clasimpset_of lthy)
-
-  fun prove_termination lthy =
-    Function.prove_termination NONE
-      (Lexicographic_Order.lexicographic_order_tac true lthy) lthy
-
   val (_, lthy') = Function.add_function all_fun_names all_fun_eqs
-    Function_Common.default_config pat_completeness_auto lthy
+    Function_Common.default_config (pat_completeness_simp constr_thms) lthy
 
   val (info, lthy'') = prove_termination (Local_Theory.restore lthy')