# HG changeset patch
# User wenzelm
# Date 1322672834 -3600
# Node ID 476ad865f1259053e03597830190b010e6f03ccf
# Parent  b108b3d7c49e14deebf371dfd364946ad269743b
prefer typedef without alternative name;

diff -r b108b3d7c49e -r 476ad865f125 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Wed Nov 30 17:30:01 2011 +0100
+++ b/src/HOL/Nat.thy	Wed Nov 30 18:07:14 2011 +0100
@@ -35,7 +35,8 @@
   Zero_RepI: "Nat Zero_Rep"
 | Suc_RepI: "Nat i \<Longrightarrow> Nat (Suc_Rep i)"
 
-typedef (open Nat) nat = "{n. Nat n}"
+typedef (open) nat = "{n. Nat n}"
+  morphisms Rep_Nat Abs_Nat
   using Nat.Zero_RepI by auto
 
 lemma Nat_Rep_Nat:
diff -r b108b3d7c49e -r 476ad865f125 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Nov 30 17:30:01 2011 +0100
+++ b/src/HOL/Product_Type.thy	Wed Nov 30 18:07:14 2011 +0100
@@ -132,8 +132,10 @@
 definition Pair_Rep :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where
   "Pair_Rep a b = (\<lambda>x y. x = a \<and> y = b)"
 
-typedef ('a, 'b) prod (infixr "*" 20) = "{f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}"
-  by auto
+definition "prod = {f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}"
+
+typedef (open) ('a, 'b) prod (infixr "*" 20) = "prod :: ('a \<Rightarrow> 'b \<Rightarrow> bool) set"
+  unfolding prod_def by auto
 
 type_notation (xsymbols)
   "prod"  ("(_ \<times>/ _)" [21, 20] 20)