# HG changeset patch
# User haftmann
# Date 1184934820 -7200
# Node ID 83b0f2518380910727b8e8be040dc5400acec77e
# Parent  851c74f1bb696129f28a8775066a7605150b0978
dropped Nat.ML legacy bindings

diff -r 851c74f1bb69 -r 83b0f2518380 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Jul 20 14:28:25 2007 +0200
+++ b/src/HOL/IsaMakefile	Fri Jul 20 14:33:40 2007 +0200
@@ -87,7 +87,7 @@
   Dense_Linear_Order.thy Divides.thy Equiv_Relations.thy Extraction.thy	\
   Finite_Set.thy FixedPoint.thy Fun.thy FunDef.thy HOL.thy		\
   Hilbert_Choice.thy Inductive.thy IntArith.thy IntDef.thy IntDiv.thy	\
-  Lattices.thy List.thy Main.thy Map.thy Nat.ML Nat.thy NatBin.thy	\
+  Lattices.thy List.thy Main.thy Map.thy Nat.thy NatBin.thy	\
   Numeral.thy OrderedGroup.thy Orderings.thy Power.thy PreList.thy	\
   Predicate.thy Product_Type.thy ROOT.ML Recdef.thy			\
   Record.thy Refute.thy Relation.thy Relation_Power.thy			\