# HG changeset patch
# User berghofe
# Date 908984327 -7200
# Node ID b4f2e281a9073781748b433a1559a117cfef1eaf
# Parent  27d4fcf5fe5f6997d2284c7eef3a751b18114994
Changed syntax of rep_datatype.

diff -r 27d4fcf5fe5f -r b4f2e281a907 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Wed Oct 21 16:38:46 1998 +0200
+++ b/src/HOL/Datatype.thy	Wed Oct 21 17:38:47 1998 +0200
@@ -7,13 +7,12 @@
 Datatype = Univ +
 
 rep_datatype sum
-  distinct "[[Inl_not_Inr, Inr_not_Inl]]"
-  inject   "[[Inl_eq, Inr_eq]]"
+  distinct Inl_not_Inr, Inr_not_Inl
+  inject   Inl_eq, Inr_eq
   induct   sum_induct
 
 rep_datatype prod
-  distinct "[[]]"
-  inject   "[[Pair_eq]]"
-  induct   "allI RS (allI RS (split_paired_All RS iffD2)) RS spec"
+  inject   Pair_eq
+  induct   prod_induct
 
 end
diff -r 27d4fcf5fe5f -r b4f2e281a907 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Wed Oct 21 16:38:46 1998 +0200
+++ b/src/HOL/Nat.thy	Wed Oct 21 17:38:47 1998 +0200
@@ -12,8 +12,8 @@
   DatatypePackage.setup
 
 rep_datatype nat
-  distinct "[[Suc_not_Zero, Zero_not_Suc]]"
-  inject   "[[Suc_Suc_eq]]"
+  distinct Suc_not_Zero, Zero_not_Suc
+  inject   Suc_Suc_eq
   induct   nat_induct
 
 instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)