--- a/Quot/Nominal/Test.thy	Thu Jan 28 09:28:20 2010 +0100
+++ b/Quot/Nominal/Test.thy	Thu Jan 28 10:26:36 2010 +0100
@@ -167,10 +167,18 @@
   val _ = warning (implode (separate "\n" (map (single_dt lthy) dts)));
   val _ = warning (implode (separate "\n" (map single_fun_fix funs)));
   val _ = warning (implode (separate "\n" (map (single_fun_eq lthy) feqs)));
+in
+  ()
+end
+*}
+
+ML {*
+fun fv_dts  (dts, (funs, feqs)) lthy =
+let
   val _ = warning (implode (separate "\n" (map (fv_dt lthy (map dt_name dts)) dts)));
 in
   lthy
-end   
+end
 *}
 
 ML {*
@@ -201,7 +209,13 @@
 ML {*
 fun fn_defn [] [] lthy = lthy
   | fn_defn funs feqs lthy =
-      Function_Fun.add_fun  Function_Common.default_config funs feqs false lthy
+      Function_Fun.add_fun Function_Common.default_config funs feqs false lthy
+*}
+
+ML {*
+fun fn_defn_cmd [] [] lthy = lthy
+  | fn_defn_cmd funs feqs lthy =
+      Function_Fun.add_fun_cmd Function_Common.default_config funs feqs false lthy
 *}
 
 ML {*
@@ -209,20 +223,21 @@
 let
   val thy' = dt_defn (map transp_dt dts) thy
   val lthy = Theory_Target.init NONE thy'
+  val lthy' = fn_defn_cmd funs feqs lthy
   fun parse_fun (b, NONE, m) = (b, NONE, m)
-    | parse_fun (b, SOME ty, m) = (b, SOME (Syntax.read_typ lthy ty), m);
+    | parse_fun (b, SOME ty, m) = (b, SOME (Syntax.read_typ lthy' ty), m);
   val funs = map parse_fun funs
-  fun parse_feq (b, t) = (b, Syntax.read_prop lthy t);
+  fun parse_feq (b, t) = (b, Syntax.read_prop lthy' t);
   val feqs = map parse_feq feqs
-  fun parse_anno_ty (anno, ty) = (anno, Syntax.read_typ lthy ty);
+  fun parse_anno_ty (anno, ty) = (anno, Syntax.read_typ lthy' ty);
   fun parse_constr (((constr_name, ty_args), bind), mx) =
     (((constr_name, map parse_anno_ty ty_args), bind), mx);
   fun parse_dt (((ty_args, ty_name), mx), constrs) =
    (((ty_args, ty_name), mx), map parse_constr constrs);
   val dts = map parse_dt dts
+  val _ = print_dts (dts, (funs, feqs)) lthy
 in
-   fn_defn funs feqs lthy
-|> print_dts (dts, (funs, feqs))
+   fv_dts (dts, (funs, feqs)) lthy
 |> Local_Theory.exit_global
 end
 *}
@@ -263,7 +278,7 @@
 binder
   f::"pat \<Rightarrow> name set"
 where 
-  "f PN = ({} :: name set)"
+  "f PN = {}"
 | "f (PS x) = {x}"
 | "f (PD (x,y)) = {x,y}"
 
@@ -279,9 +294,9 @@
 binder
   f2::"pat2 \<Rightarrow> name set"
 where 
-  "f2 PN2 = ({} :: name set)"
+  "f2 PN2 = {}"
 | "f2 (PS2 x) = {x}"
-| "f2 (PD2 (p1, p2)) = (f2 p1) \<union> (f2 p2 :: name set)"
+| "f2 (PD2 (p1, p2)) = (f2 p1) \<union> (f2 p2)"
 
 text {* example type schemes *}
 datatype ty =