# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1272550549 -7200
# Node ID 522748f37444ad86ec4bd3256b2cb55786478686
# Parent  727e0edad2847151befd05dcb34bb907fe69aa44
Extracting the fv body function and exporting the terms.

diff -r 727e0edad284 -r 522748f37444 Nominal/NewFv.thy
--- a/Nominal/NewFv.thy	Thu Apr 29 13:19:12 2010 +0200
+++ b/Nominal/NewFv.thy	Thu Apr 29 16:15:49 2010 +0200
@@ -82,22 +82,25 @@
 *}
 
 ML {*
+fun fv_body thy dts args fv_frees supp i =
+let
+  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 (if supp then mk_supp x else atoms thy x)
+end
+*}
+
+ML {*
 fun fv_bm_lsts thy dts args fv_frees bn_fvbn binds bodys =
 let
-  fun fv_body supp i =
-    let
-      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 (if supp then mk_supp x else atoms thy x)
-    end
-  val fv_bodys = mk_union (map (fv_body true) bodys)
+  val fv_bodys = mk_union (map (fv_body thy dts args fv_frees true) bodys)
   val bound_vars =
     case binds of
       [(SOME bn, i)] => setify (bn $ nth args i)
-    | _ => mk_union (map (fv_body false) (map snd binds));
+    | _ => mk_union (map (fv_body thy dts args fv_frees false) (map snd binds));
   val non_rec_vars =
     case binds of
       [(SOME bn, i)] =>
@@ -206,9 +209,6 @@
 *}
 
 ML {*
-*}
-
-ML {*
 fun define_raw_fv (dt_info : Datatype_Aux.info) bn_funs bclausesss lthy =
 let
   val thy = ProofContext.theory_of lthy;
@@ -221,7 +221,7 @@
   val (bn_fvbn, fv_bn_names, fv_bn_eqs) =
     fv_bns thy dt_descr sorts fv_frees bn_funs bclausesss;
 
-  val fvbns = map snd bn_fvbn;
+  val fv_bns = 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) bclausesss (fv_frees ~~ fv_nums);
@@ -241,8 +241,13 @@
     Function_Common.default_config pat_completeness_auto lthy
 
   val lthy'' = prove_termination (Local_Theory.restore lthy')
+
+  val morphism = ProofContext.export_morphism lthy'' lthy
+  val fv_frees_exp = map (Morphism.term morphism) fv_frees
+  val fv_bns_exp = map (Morphism.term morphism) fv_bns
+
 in
-  ((fv_frees, fvbns), info, lthy'')
+  ((fv_frees_exp, fv_bns_exp), info, lthy'')
 end
 *}