--- 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)"
--- 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.
--- 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
--- 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
--- 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;
-