revert debugging output that shouldn't have been submitted in the first place
authorblanchet
Wed, 24 Mar 2010 14:51:36 +0100
changeset 35970 3d41a2a490f0
parent 35969 c9565298df9e
child 35971 4f24a4e9af4a
revert debugging output that shouldn't have been submitted in the first place
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- 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