--- a/src/HOL/Product_Type.thy Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Product_Type.thy Fri Feb 14 07:53:46 2014 +0100
@@ -12,7 +12,7 @@
subsection {* @{typ bool} is a datatype *}
-wrap_free_constructors [True, False] case_bool [=]
+free_constructors [True, False] case_bool [=]
by auto
text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
@@ -23,7 +23,7 @@
setup {* Sign.parent_path *}
-text {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
+text {* But erase the prefix for properties that are not generated by @{text free_constructors}. *}
setup {* Sign.mandatory_path "bool" *}
@@ -82,7 +82,7 @@
else SOME (mk_meta_eq @{thm unit_eq})
*}
-wrap_free_constructors ["()"] case_unit
+free_constructors ["()"] case_unit
by auto
text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
@@ -93,7 +93,7 @@
setup {* Sign.parent_path *}
-text {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
+text {* But erase the prefix for properties that are not generated by @{text free_constructors}. *}
setup {* Sign.mandatory_path "unit" *}
@@ -184,7 +184,7 @@
lemma prod_cases: "(\<And>a b. P (Pair a b)) \<Longrightarrow> P p"
by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def)
-wrap_free_constructors [Pair] case_prod [] [[fst, snd]]
+free_constructors [Pair] case_prod [] [[fst, snd]]
proof -
fix P :: bool and p :: "'a \<times> 'b"
show "(\<And>x1 x2. p = Pair x1 x2 \<Longrightarrow> P) \<Longrightarrow> P"
@@ -208,7 +208,7 @@
setup {* Sign.parent_path *}
-text {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
+text {* But erase the prefix for properties that are not generated by @{text free_constructors}. *}
setup {* Sign.mandatory_path "prod" *}