# HG changeset patch
# User paulson
# Date 957446206 -7200
# Node ID a735b1e74f3a1d7f10e0ea8fe8c4791e788ed9e7
# Parent  59a4b5e6a591c5ebbe20f8bc826931cb6580b1fc
of course it should use Main

diff -r 59a4b5e6a591 -r a735b1e74f3a src/HOL/Quot/NPAIR.thy
--- a/src/HOL/Quot/NPAIR.thy	Thu May 04 15:16:18 2000 +0200
+++ b/src/HOL/Quot/NPAIR.thy	Thu May 04 15:16:46 2000 +0200
@@ -6,7 +6,7 @@
 Example: define a PER on pairs of natural numbers (with embedding)
 
 *)
-NPAIR = PER + Datatype + (* representation for rational numbers *)
+NPAIR = PER + Main + (* representation for rational numbers *)
 
 datatype NP = abs_NP "(nat * nat)"