1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Mar 24 14:51:36 2010 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Mar 25 17:55:55 2010 +0100
     1.3 @@ -11,13 +11,13 @@
     1.4    val default_params : theory -> (string * string) list -> params
     1.5  end;
     1.6  
     1.7 -structure Sledgehammer_Isar : sig end =
     1.8 +structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
     1.9  struct
    1.10  
    1.11 +open Sledgehammer_Util
    1.12  open ATP_Manager
    1.13  open ATP_Minimal
    1.14  open ATP_Wrapper
    1.15 -open Sledgehammer_Util
    1.16  
    1.17  structure K = OuterKeyword and P = OuterParse
    1.18  
    1.19 @@ -55,12 +55,12 @@
    1.20     ("dont_follow_defs", "follow_defs"),
    1.21     ("metis_proof", "isar_proof")]
    1.22  
    1.23 -val property_affected_params = ["atps", "full_types", "timeout"]
    1.24 +val property_dependent_params = ["atps", "full_types", "timeout"]
    1.25  
    1.26  fun is_known_raw_param s =
    1.27    AList.defined (op =) default_default_params s orelse
    1.28    AList.defined (op =) negated_params s orelse
    1.29 -  member (op =) property_affected_params s
    1.30 +  member (op =) property_dependent_params s
    1.31  
    1.32  fun check_raw_param (s, _) =
    1.33    if is_known_raw_param s then ()