# HG changeset patch
# User wenzelm
# Date 877706733 -7200
# Node ID 0614fdf0db2065cc615c2de28213ad74a0e5ed11
# Parent  86c5bda38e9f5bd0317b6df00fb648006516e8be
ProtoPure.flexpair_def;

diff -r 86c5bda38e9f -r 0614fdf0db20 src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Fri Oct 24 17:19:14 1997 +0200
+++ b/src/HOL/NatDef.ML	Fri Oct 24 17:25:33 1997 +0200
@@ -77,7 +77,7 @@
   exhaustion = natE,
   exhaust_tac = fn v => ALLNEWSUBGOALS (res_inst_tac [("n",v)] natE)
                                        (rotate_tac ~1),
-  nchotomy = flexpair_def, case_cong = flexpair_def})];
+  nchotomy = ProtoPure.flexpair_def, case_cong = ProtoPure.flexpair_def})];
 
 
 (*** Isomorphisms: Abs_Nat and Rep_Nat ***)