1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Aug 31 21:17:19 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Aug 31 22:27:33 2010 +0200
     1.3 @@ -63,7 +63,8 @@
     1.4  type raw_param = string * string list
     1.5  
     1.6  val default_default_params =
     1.7 -  [("debug", "false"),
     1.8 +  [("blocking", "false"),
     1.9 +   ("debug", "false"),
    1.10     ("verbose", "false"),
    1.11     ("overlord", "false"),
    1.12     ("explicit_apply", "false"),
    1.13 @@ -76,7 +77,8 @@
    1.14  val alias_params =
    1.15    [("atp", "atps")]
    1.16  val negated_alias_params =
    1.17 -  [("no_debug", "debug"),
    1.18 +  [("non_blocking", "blocking"),
    1.19 +   ("no_debug", "debug"),
    1.20     ("quiet", "verbose"),
    1.21     ("no_overlord", "overlord"),
    1.22     ("partial_types", "full_types"),
    1.23 @@ -167,6 +169,7 @@
    1.24        case lookup name of
    1.25          SOME "smart" => NONE
    1.26        | _ => SOME (lookup_int name)
    1.27 +    val blocking = lookup_bool "blocking"
    1.28      val debug = lookup_bool "debug"
    1.29      val verbose = debug orelse lookup_bool "verbose"
    1.30      val overlord = lookup_bool "overlord"
    1.31 @@ -182,8 +185,8 @@
    1.32      val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
    1.33      val timeout = lookup_time "timeout"
    1.34    in
    1.35 -    {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
    1.36 -     full_types = full_types, explicit_apply = explicit_apply,
    1.37 +    {blocking = blocking, debug = debug, verbose = verbose, overlord = overlord,
    1.38 +     atps = atps, full_types = full_types, explicit_apply = explicit_apply,
    1.39       relevance_thresholds = relevance_thresholds, max_relevant = max_relevant,
    1.40       theory_relevant = theory_relevant, isar_proof = isar_proof,
    1.41       isar_shrink_factor = isar_shrink_factor, timeout = timeout}