--- a/Quot/Nominal/Test.thy	Wed Jan 27 13:44:05 2010 +0100
+++ b/Quot/Nominal/Test.thy	Wed Jan 27 14:56:58 2010 +0100
@@ -99,6 +99,13 @@
    ^ (Pretty.str_of (Syntax.pretty_mixfix syn)))
 *}
 
+ML Local_Theory.exit_global
+
+ML {*
+fun fv_constr prefix (((name, anno_tys), bds), syn) =
+  prefix ^ " (" ^ (Binding.name_of name) ^ ") = "
+*}
+
 ML {*
 fun single_dt (((s2, s3), syn), constrs) =
    ["constructor declaration"]
@@ -110,6 +117,13 @@
  |> implode
 *}
 
+ML {*
+fun fv_dt (((s2, s3), syn), constrs) =
+    map (fv_constr ("fv_" ^ Binding.name_of s3)) constrs
+ |> separate "\n"
+ |> implode
+*}
+
 ML {* fun single_fun_eq (at, s) = 
   ["function equations: ", s] 
   |> separate "\n"
@@ -123,11 +137,12 @@
 *}
 
 ML {*
-fun print_dts (dts, (funs, feqs)) = 
+fun print_dts (dts, (funs, feqs)) lthy = 
 let
    val _ = warning (implode (separate "\n" (map single_dt dts)))
    val _ = warning (implode (separate "\n" (map single_fun_fix funs)))
    val _ = warning (implode (separate "\n" (map single_fun_eq feqs)))
+   val _ = warning (implode (separate "\n" (map fv_dt dts)))
 in
   ()
 end   
@@ -163,8 +178,8 @@
   | fn_defn funs feqs thy =
 let
   val lthy = Theory_Target.init NONE thy
-  val ctxt = Function_Fun.add_fun_cmd  Function_Common.default_config funs feqs false lthy
-  val thy' = ProofContext.theory_of ctxt
+  val lthy = Function_Fun.add_fun_cmd  Function_Common.default_config funs feqs false lthy
+  val thy' = Local_Theory.exit_global ctxt
 in
   thy'
 end
@@ -173,13 +188,12 @@
 
 ML {*
 fun nominal_datatype2_cmd (dts, (funs, feqs)) thy =
-let
-  val thy1 = dt_defn (map transp_dt dts) thy
-  val thy2 = fn_defn funs feqs thy1
-  val _ = print_dts (dts, (funs, feqs)) 
-in
-  thy2
-end *}
+   dt_defn (map transp_dt dts) thy
+|> fn_defn funs feqs
+|> Theory_Target.init NONE
+|> print_dts (dts, (funs, feqs))
+|> Local_Theory.exit_global
+*}
 
 (* Command Keyword *)
 ML {*