changeset 55968 | 94242fa87638 |
parent 55466 | 786edc984c98 |
child 56248 | 67dc9549fa15 |
--- a/src/HOL/Fun_Def.thy Fri Mar 07 12:35:06 2014 +0000 +++ b/src/HOL/Fun_Def.thy Fri Mar 07 14:21:15 2014 +0100 @@ -83,7 +83,6 @@ by (simp add: wfP_def) ML_file "Tools/Function/function_core.ML" -ML_file "Tools/Function/sum_tree.ML" ML_file "Tools/Function/mutual.ML" ML_file "Tools/Function/pattern_split.ML" ML_file "Tools/Function/relation.ML"