diff -r 045c96e3edf0 -r 1bfed12a7646 src/HOL/Fun_Def.thy
--- a/src/HOL/Fun_Def.thy	Sat Aug 16 19:01:31 2014 +0200
+++ b/src/HOL/Fun_Def.thy	Sat Aug 16 19:20:11 2014 +0200
@@ -117,8 +117,8 @@
 inductive is_measure :: "('a \<Rightarrow> nat) \<Rightarrow> bool"
 where is_measure_trivial: "is_measure f"
 
+named_theorems measure_function "rules that guide the heuristic generation of measure functions"
 ML_file "Tools/Function/measure_functions.ML"
-setup MeasureFunctions.setup
 
 lemma measure_size[measure_function]: "is_measure size"
 by (rule is_measure_trivial)