# HG changeset patch
# User blanchet
# Date 1269438696 -3600
# Node ID 3d41a2a490f0351defb96d9ff2c4e1f852cf719e
# Parent  c9565298df9e037093333300ca24515ffccf7b9c
revert debugging output that shouldn't have been submitted in the first place

diff -r c9565298df9e -r 3d41a2a490f0 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.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))
diff -r c9565298df9e -r 3d41a2a490f0 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- 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