src/HOL/ex/sledgehammer_tactics.ML
changeset 42449 494e4ac5b0f8
parent 42444 8e5438dc70bb
child 42579 2552c09b1a72
     1.1 --- a/src/HOL/ex/sledgehammer_tactics.ML	Thu Apr 21 21:14:06 2011 +0200
     1.2 +++ b/src/HOL/ex/sledgehammer_tactics.ML	Thu Apr 21 22:18:28 2011 +0200
     1.3 @@ -33,7 +33,7 @@
     1.4      val relevance_override = {add = [], del = [], only = false}
     1.5      val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
     1.6      val no_dangerous_types =
     1.7 -      Sledgehammer_ATP_Translate.types_dangerous_types type_sys
     1.8 +      Sledgehammer_ATP_Translate.type_system_types_dangerous_types type_sys
     1.9      val facts =
    1.10        Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types
    1.11            relevance_thresholds