# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264604869 -3600
# Node ID 362402adfb882831ffb5ddd6845d14f4eb807df2
# Parent  67739818af3fa6cba7fcf1af2e3e598ab54d1eb8
Undid the parsing, as it is not possible with thy->lthy interaction.

diff -r 67739818af3f -r 362402adfb88 Quot/Nominal/Test.thy
--- a/Quot/Nominal/Test.thy	Wed Jan 27 14:57:11 2010 +0100
+++ b/Quot/Nominal/Test.thy	Wed Jan 27 16:07:49 2010 +0100
@@ -139,12 +139,12 @@
 ML {*
 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)))
+  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
-  ()
+  lthy
 end   
 *}
 
@@ -174,23 +174,17 @@
 *}
 
 ML {*
-fun fn_defn [] [] thy = thy
-  | fn_defn funs feqs thy =
-let
-  val lthy = Theory_Target.init NONE thy
-  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
+fun fn_defn [] [] lthy = lthy
+  | fn_defn funs feqs lthy =
+      Function_Fun.add_fun_cmd Function_Common.default_config funs feqs false lthy
 *}
 
 
 ML {*
 fun nominal_datatype2_cmd (dts, (funs, feqs)) thy =
    dt_defn (map transp_dt dts) thy
+|> Theory_Target.init NONE
 |> fn_defn funs feqs
-|> Theory_Target.init NONE
 |> print_dts (dts, (funs, feqs))
 |> Local_Theory.exit_global
 *}