# HG changeset patch
# User blanchet
# Date 1377855442 -7200
# Node ID cfef783090ebf5d32fd84f51f34e19a0bce86de6
# Parent  ae49b835ca01ca2d2fe173748d5ba0eb596f17e7
polished newly included files after moving

diff -r ae49b835ca01 -r cfef783090eb src/HOL/BNF/BNF_FP_N2M.thy
--- a/src/HOL/BNF/BNF_FP_N2M.thy	Fri Aug 30 11:27:23 2013 +0200
+++ b/src/HOL/BNF/BNF_FP_N2M.thy	Fri Aug 30 11:37:22 2013 +0200
@@ -9,7 +9,7 @@
 header {* Flattening of Nested to Mutual (Co)recursion *}
 
 theory BNF_FP_N2M
-imports "~~/src/HOL/BNF/BNF_FP_Basic"
+imports BNF_FP_Basic
 begin
 
 lemma eq_le_Grp_id_iff: "(op = \<le> BNF_Util.Grp (Collect R) id) = (All R)"
diff -r ae49b835ca01 -r cfef783090eb src/HOL/BNF/BNF_FP_Rec_Sugar.thy
--- a/src/HOL/BNF/BNF_FP_Rec_Sugar.thy	Fri Aug 30 11:27:23 2013 +0200
+++ b/src/HOL/BNF/BNF_FP_Rec_Sugar.thy	Fri Aug 30 11:37:22 2013 +0200
@@ -1,7 +1,7 @@
 (*  Title:      HOL/BNF/BNF_FP_Rec_Sugar.thy
     Author:     Lorenz Panny, TU Muenchen
+    Author:     Jasmin Blanchette, TU Muenchen
     Author:     Dmitriy Traytel, TU Muenchen
-    Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2013
 
 Recursor and corecursor sugar.
diff -r ae49b835ca01 -r cfef783090eb src/HOL/BNF/Examples/Misc_Primrec.thy
--- a/src/HOL/BNF/Examples/Misc_Primrec.thy	Fri Aug 30 11:27:23 2013 +0200
+++ b/src/HOL/BNF/Examples/Misc_Primrec.thy	Fri Aug 30 11:37:22 2013 +0200
@@ -8,9 +8,7 @@
 header {* Miscellaneous Primitive Recursive Function Definitions *}
 
 theory Misc_Primrec
-imports
-  "~~/src/HOL/BNF/Examples/Misc_Datatype"
-  "../BNF_FP_Rec_Sugar"
+imports Misc_Datatype
 begin
 
 primrec_new nat_of_simple :: "simple \<Rightarrow> nat" where
diff -r ae49b835ca01 -r cfef783090eb src/HOL/BNF/Tools/bnf_fp_n2m.ML
--- a/src/HOL/BNF/Tools/bnf_fp_n2m.ML	Fri Aug 30 11:27:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m.ML	Fri Aug 30 11:37:22 2013 +0200
@@ -374,9 +374,6 @@
         xtor_co_iter_o_map_thmss = steal #xtor_co_iter_o_map_thmss (*theorem about old constant*),
         rel_xtor_co_induct_thm = rel_xtor_co_induct_thm}
        |> morph_fp_result (Morphism.term_morphism (singleton (Variable.polymorphic lthy))));
-(**
-    val _ = fp_res |> @{make_string} |> tracing
-**)
   in
     (fp_res, lthy)
   end
diff -r ae49b835ca01 -r cfef783090eb src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Fri Aug 30 11:27:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Fri Aug 30 11:37:22 2013 +0200
@@ -47,7 +47,7 @@
 };
 
 fun permute_args n t = list_comb (t, map Bound (0 :: (n downto 1)))
-  |> fold (K (fn u => Abs ("", dummyT, u))) (0 upto n);
+  |> fold (K (fn u => Abs (Name.uu, dummyT, u))) (0 upto n);
 
 fun dissect_eqn lthy fun_names eqn' =
   let
@@ -674,7 +674,7 @@
     fun currys Ts t = if length Ts <= 1 then t else
       t $ foldr1 (fn (u, v) => HOLogic.pair_const dummyT dummyT $ u $ v)
         (length Ts - 1 downto 0 |> map Bound)
-      |> fold_rev (fn T => fn u => Abs ("", T, u)) Ts;
+      |> fold_rev (fn T => fn u => Abs (Name.uu, T, u)) Ts;
   in
     map (list_comb o rpair corec_args) corecs
     |> map2 (fn Ts => fn t => if length Ts = 0 then t $ HOLogic.unit else t) arg_Tss
@@ -741,4 +741,3 @@
     uncurry add_primcorec_cmd);
 
 end;
-