changeset 30927 | bc51b343f80d |
parent 30609 | 983e8b6e4e69 |
child 30929 | d9343c0aac11 |
--- a/src/HOL/HOL.thy Wed Apr 15 15:34:00 2009 +0200 +++ b/src/HOL/HOL.thy Wed Apr 15 15:34:54 2009 +0200 @@ -29,7 +29,6 @@ ("~~/src/Tools/induct_tacs.ML") "~~/src/Tools/value.ML" "~~/src/Tools/code/code_name.ML" - "~~/src/Tools/code/code_funcgr.ML" (*formal dependency*) "~~/src/Tools/code/code_wellsorted.ML" "~~/src/Tools/code/code_thingol.ML" "~~/src/Tools/code/code_printer.ML"