# HG changeset patch
# User haftmann
# Date 1235294549 -3600
# Node ID 05354c653d3abceee198df971841cae1b0d36078
# Parent  00d04a562df1a3784716263cdf2e9eaa6a9105e5
formal dependency on newly emerging algorithm

diff -r 00d04a562df1 -r 05354c653d3a src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Feb 20 21:29:34 2009 +0100
+++ b/src/HOL/HOL.thy	Sun Feb 22 10:22:29 2009 +0100
@@ -28,6 +28,7 @@
   ("~~/src/Tools/induct_tacs.ML")
   "~~/src/Tools/value.ML"
   "~~/src/Tools/code/code_name.ML"
+  "~~/src/Tools/code/code_wellsorted.ML" (* formal dependency *)
   "~~/src/Tools/code/code_funcgr.ML"
   "~~/src/Tools/code/code_thingol.ML"
   "~~/src/Tools/code/code_printer.ML"
diff -r 00d04a562df1 -r 05354c653d3a src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Feb 20 21:29:34 2009 +0100
+++ b/src/HOL/IsaMakefile	Sun Feb 22 10:22:29 2009 +0100
@@ -86,7 +86,7 @@
   Tools/simpdata.ML \
   $(SRC)/Tools/atomize_elim.ML \
   $(SRC)/Tools/code/code_funcgr.ML \
-  $(SRC)/Tools/code/code_funcgr.ML \
+  $(SRC)/Tools/code/code_wellsorted.ML \
   $(SRC)/Tools/code/code_name.ML \
   $(SRC)/Tools/code/code_printer.ML \
   $(SRC)/Tools/code/code_target.ML \