| changeset 30013 | 1e0b8e561cc2 | 
| parent 30006 | f54b48cda286 | 
| child 30049 | 05354c653d3a | 
--- a/src/HOL/HOL.thy Fri Feb 20 14:49:23 2009 +0100 +++ b/src/HOL/HOL.thy Fri Feb 20 14:49:24 2009 +0100 @@ -28,7 +28,7 @@ ("~~/src/Tools/induct_tacs.ML") "~~/src/Tools/value.ML" "~~/src/Tools/code/code_name.ML" - "~~/src/Tools/code/code_wellsorted.ML" + "~~/src/Tools/code/code_funcgr.ML" "~~/src/Tools/code/code_thingol.ML" "~~/src/Tools/code/code_printer.ML" "~~/src/Tools/code/code_target.ML"