diff -r 95b2626c75a8 -r 494e4ac5b0f8 src/HOL/ex/sledgehammer_tactics.ML
--- a/src/HOL/ex/sledgehammer_tactics.ML	Thu Apr 21 21:14:06 2011 +0200
+++ b/src/HOL/ex/sledgehammer_tactics.ML	Thu Apr 21 22:18:28 2011 +0200
@@ -33,7 +33,7 @@
     val relevance_override = {add = [], del = [], only = false}
     val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
     val no_dangerous_types =
-      Sledgehammer_ATP_Translate.types_dangerous_types type_sys
+      Sledgehammer_ATP_Translate.type_system_types_dangerous_types type_sys
     val facts =
       Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types
           relevance_thresholds