--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Mar 24 14:49:32 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Mar 24 14:51:36 2010 +0100
@@ -568,9 +568,6 @@
create additional clauses based on the information from extra_cls *)
fun prepare_clauses higher_order dfg goal_cls chain_ths axcls extra_cls thy =
let
-(* ### *)
-val _ = priority ("prepare clauses: axiom " ^ Int.toString (length axcls) ^
- ", extra " ^ Int.toString (length extra_cls))
(* add chain thms *)
val chain_cls =
cnf_rules_pairs thy (filter check_named (map pairname chain_ths))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Mar 24 14:49:32 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Mar 24 14:51:36 2010 +0100
@@ -99,7 +99,7 @@
val lookup_string = the_default "" o lookup
fun general_lookup_bool option default_value name =
case lookup name of
- SOME s => s |> parse_bool_option option name
+ SOME s => parse_bool_option option name s
| NONE => default_value
val lookup_bool = the o general_lookup_bool false (SOME false)
val lookup_bool_option = general_lookup_bool true NONE