# HG changeset patch
# User blanchet
# Date 1282917855 -7200
# Node ID 91ad85f962c48e28c3c00dec54eb60e48cf0ef01
# Parent  cf01645cbbcecee32fe0450319057287998ef71c
turn off experimental feature per default + avoid exception on "theory constant"

diff -r cf01645cbbce -r 91ad85f962c4 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Aug 27 15:39:17 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Aug 27 16:04:15 2010 +0200
@@ -31,7 +31,8 @@
 val trace = Unsynchronized.ref false
 fun trace_msg msg = if !trace then tracing (msg ()) else ()
 
-val term_patterns = Unsynchronized.ref true
+(* experimental feature *)
+val term_patterns = Unsynchronized.ref false
 
 val respect_no_atp = true
 
@@ -105,7 +106,8 @@
   | _ => PApp ("?", [])  (* equivalence class of higher-order constructs *)
 (* Pairs a constant with the list of its type instantiations. *)
 and pconst_args thy const (s, T) ts =
-  (if const then map ptype (Sign.const_typargs thy (s, T)) else []) @
+  (if const then map ptype (these (try (Sign.const_typargs thy) (s, T)))
+   else []) @
   (if !term_patterns then map (pterm thy) ts else [])
 and pconst thy const (s, T) ts = (s, pconst_args thy const (s, T) ts)