--- a/Nominal/NewFv.thy	Thu Apr 29 10:11:48 2010 +0200
+++ b/Nominal/NewFv.thy	Thu Apr 29 10:59:08 2010 +0200
@@ -1,6 +1,6 @@
 theory NewFv
-imports "../Nominal-General/Nominal2_Atoms" 
-        "Abs" "Perm" "Rsp" "Nominal2_FSet"
+imports "../Nominal-General/Nominal2_Atoms"
+        "Abs" "Perm" "Nominal2_FSet"
 begin
 
 ML {*
@@ -75,6 +75,11 @@
 *}
 
 ML {*
+fun mk_supp t =
+  Const (@{const_name supp}, fastype_of t --> @{typ "atom set"}) $ t
+*}
+
+ML {*
 fun setify x =
   if fastype_of x = @{typ "atom list"} 
   then @{term "set::atom list \<Rightarrow> atom set"} $ x 
@@ -89,9 +94,9 @@
       val x = nth args i;
       val dt = nth dts i;
     in
-      if Datatype_Aux.is_rec_type dt 
-      then nth fv_frees (Datatype_Aux.body_index dt) $ x 
-      else atoms thy x
+      if Datatype_Aux.is_rec_type dt
+      then nth fv_frees (Datatype_Aux.body_index dt) $ x
+      else mk_supp x
     end
   val fv_bodys = mk_union (map fv_body bodys)
   val bound_vars =
@@ -119,9 +124,9 @@
       val dt = nth dts i;
     in
       case AList.lookup (op=) args_in_bn i of
-        NONE => if Datatype_Aux.is_rec_type dt 
-                then nth fv_frees (Datatype_Aux.body_index dt) $ x 
-                else atoms thy x
+        NONE => if Datatype_Aux.is_rec_type dt
+                then nth fv_frees (Datatype_Aux.body_index dt) $ x
+                else mk_supp x
       | SOME (SOME (f : term)) => (the (AList.lookup (op=) bn_fvbn f)) $ x
       | SOME NONE => noatoms
     end
@@ -131,9 +136,9 @@
 *}
 
 ML {*
-fun fv_bn thy dt_descr sorts fv_frees bn_fvbn bmll (fvbn, (_, ith_dtyp, args_in_bns)) =
+fun fv_bn thy dt_descr sorts fv_frees bn_fvbn bclausess (fvbn, (_, ith_dtyp, args_in_bns)) =
 let
-  fun fv_bn_constr (cname, dts) (args_in_bn, bml) =
+  fun fv_bn_constr (cname, dts) (args_in_bn, bclauses) =
   let
     val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts;
     val names = Datatype_Prop.make_tnames Ts;
@@ -142,16 +147,16 @@
     val fv_bn_bm = fv_bn_bm thy dts args fv_frees bn_fvbn args_in_bn
   in
     HOLogic.mk_Trueprop (HOLogic.mk_eq
-      (fvbn $ list_comb (c, args), mk_union (map fv_bn_bm bml)))
+      (fvbn $ list_comb (c, args), mk_union (map fv_bn_bm bclauses)))
   end;
   val (_, (_, _, constrs)) = nth dt_descr ith_dtyp;
 in
-  map2 fv_bn_constr constrs (args_in_bns ~~ bmll)
+  map2 fv_bn_constr constrs (args_in_bns ~~ bclausess)
 end
 *}
 
 ML {*
-fun fv_bns thy dt_descr sorts fv_frees bn_funs bclauses =
+fun fv_bns thy dt_descr sorts fv_frees bn_funs bclausesss =
 let
   fun mk_fvbn_free (bn, ith, _) =
     let
@@ -161,8 +166,8 @@
     end;
   val (fvbn_names, fvbn_frees) = split_list (map mk_fvbn_free bn_funs);
   val bn_fvbn = (map (fn (bn, _, _) => bn) bn_funs) ~~ fvbn_frees
-  val bmlls = map (fn (_, i, _) => nth bclauses i) bn_funs;
-  val eqs = map2 (fv_bn thy dt_descr sorts fv_frees bn_fvbn) bmlls (fvbn_frees ~~ bn_funs);
+  val bclausessl = map (fn (_, i, _) => nth bclausesss i) bn_funs;
+  val eqs = map2 (fv_bn thy dt_descr sorts fv_frees bn_fvbn) bclausessl (fvbn_frees ~~ bn_funs);
 in
   (bn_fvbn, fvbn_names, eqs)
 end
@@ -176,9 +181,9 @@
       val x = nth args i;
       val dt = nth dts i;
     in
-      if Datatype_Aux.is_rec_type dt 
-      then nth fv_frees (Datatype_Aux.body_index dt) $ x 
-      else atoms thy x
+      if Datatype_Aux.is_rec_type dt
+      then nth fv_frees (Datatype_Aux.body_index dt) $ x
+      else mk_supp x
     end
 | BLst (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
 | BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
@@ -186,9 +191,9 @@
 *}
 
 ML {*
-fun fv thy dt_descr sorts fv_frees bn_fvbn bmll (fv_free, ith_dtyp) =
+fun fv thy dt_descr sorts fv_frees bn_fvbn bclausess (fv_free, ith_dtyp) =
 let
-  fun fv_constr (cname, dts) bml =
+  fun fv_constr (cname, dts) bclauses =
   let
     val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts;
     val names = Datatype_Prop.make_tnames Ts;
@@ -197,23 +202,15 @@
     val fv_bn_bm = fv_bm thy dts args fv_frees bn_fvbn
   in
     HOLogic.mk_Trueprop (HOLogic.mk_eq
-      (fv_free $ list_comb (c, args), mk_union (map fv_bn_bm bml)))
+      (fv_free $ list_comb (c, args), mk_union (map fv_bn_bm bclauses)))
   end;
   val (_, (_, _, constrs)) = nth dt_descr ith_dtyp;
 in
-  map2 fv_constr constrs bmll
+  map2 fv_constr constrs bclausess
 end
 *}
 
 ML {*
-val by_pat_completeness_auto =
-  Proof.global_terminal_proof
-    (Method.Basic Pat_Completeness.pat_completeness,
-     SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none))))
-
-fun termination_by method =
-  Function.termination_proof NONE
-  #> Proof.global_terminal_proof (Method.Basic method, NONE)
 *}
 
 ML {*
@@ -226,25 +223,31 @@
   val fv_types = map (fn (i, _) => nth_dtyp descr sorts i --> @{typ "atom set"}) dt_descr;
   val fv_frees = map Free (fv_names ~~ fv_types);
 
-  val (bn_fvbn, fv_bn_names, fv_bn_eqs) = 
+  val (bn_fvbn, fv_bn_names, fv_bn_eqs) =
     fv_bns thy dt_descr sorts fv_frees bn_funs bclauses;
 
   val fvbns = map snd bn_fvbn;
   val fv_nums = 0 upto (length fv_frees - 1)
 
   val fv_eqs = map2 (fv thy dt_descr sorts fv_frees bn_fvbn) bclauses (fv_frees ~~ fv_nums);
-  
+
   val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
   val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs)
 
-  val lthy' =
-    lthy
-    |> Function.add_function all_fv_names all_fv_eqs Function_Common.default_config
-    |> by_pat_completeness_auto
-    |> Local_Theory.restore
-    |> termination_by (Lexicographic_Order.lexicographic_order)
+  fun pat_completeness_auto ctxt =
+    Pat_Completeness.pat_completeness_tac ctxt 1
+      THEN auto_tac (clasimpset_of ctxt)
+
+  fun prove_termination lthy =
+    Function.prove_termination NONE
+      (Lexicographic_Order.lexicographic_order_tac true lthy) lthy
+
+  val (info, lthy') = Function.add_function all_fv_names all_fv_eqs
+    Function_Common.default_config pat_completeness_auto lthy
+
+  val lthy'' = prove_termination (Local_Theory.restore lthy')
 in
-  (fv_frees @ fvbns, lthy')
+  ((fv_frees, fvbns), info, lthy'')
 end
 *}
 

--- a/Nominal/NewParser.thy	Thu Apr 29 10:11:48 2010 +0200
+++ b/Nominal/NewParser.thy	Thu Apr 29 10:59:08 2010 +0200
@@ -277,7 +277,7 @@
   val thy = Local_Theory.exit_global lthy2;
   val lthy3 = Theory_Target.init NONE thy;
 
-  val (_, lthy4) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3;
+  val ((fv, fvbn), info, lthy4) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3;
 in
   ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy4)
 end
@@ -460,11 +460,12 @@
   P1 name
 | P2 pt pt
 binder
- bn::"pt \<Rightarrow> atom set" 
+ bn::"pt \<Rightarrow> atom set"
 where
   "bn (P1 x) = {atom x}"
 | "bn (P2 p1 p2) = bn p1 \<union> bn p2"
 
+thm fv_lam_raw.simps fv_pt_raw.simps fv_bn_raw.simps
 
 nominal_datatype exp =
   EVar name