# HG changeset patch
# User paulson
# Date 1193754533 -3600
# Node ID 78f8aaa274934f39c40e4a8f4d7a81dc08e85491
# Parent  6c3890cbceac5bf9c6e3d7804da02f5b437d143c
bugfixes concerning strange theorems

diff -r 6c3890cbceac -r 78f8aaa27493 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Tue Oct 30 15:13:48 2007 +0100
+++ b/src/HOL/Tools/res_atp.ML	Tue Oct 30 15:28:53 2007 +0100
@@ -468,8 +468,8 @@
         val xname = NameSpace.extern space name;
       in
         if blacklisted name then I
-        else if is_valid (xname, ths) then cons (xname, ths)
-        else if is_valid (name, ths) then cons (name, ths)
+        else if is_valid (xname, ths) then cons (xname, filter_out ResAxioms.bad_for_atp ths)
+        else if is_valid (name, ths) then cons (name, filter_out ResAxioms.bad_for_atp ths)
         else I
       end;
     val thy = ProofContext.theory_of ctxt;
@@ -731,6 +731,8 @@
         | get_neg_subgoals (gl::gls) n = #1 (ResAxioms.neg_conjecture_clauses th n) ::
                                          get_neg_subgoals gls (n+1)
       val goal_cls = get_neg_subgoals goals 1
+                     handle THM ("assume: variables", _, _) => 
+                       error "Sledgehammer: Goal contains type variables (TVars)"                       
       val isFO = case !linkup_logic_mode of
 			  Auto => forall (Meson.is_fol_term thy) (map prop_of (List.concat goal_cls))
 			| Fol => true
diff -r 6c3890cbceac -r 78f8aaa27493 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Tue Oct 30 15:13:48 2007 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Tue Oct 30 15:28:53 2007 +0100
@@ -10,6 +10,7 @@
   val cnf_axiom: thm -> thm list
   val pairname: thm -> string * thm
   val multi_base_blacklist: string list 
+  val bad_for_atp: thm -> bool
   val cnf_rules_pairs: (string * thm) list -> (thm * (string * int)) list
   val cnf_rules_of_ths: thm list -> thm list
   val neg_clausify: thm list -> thm list
@@ -320,6 +321,14 @@
 fun too_complex t = 
   Meson.too_many_clauses t orelse excessive_lambdas_fm [] t;
   
+fun is_strange_thm th =
+  case head_of (concl_of th) of
+      Const (a,_) => (a <> "Trueprop" andalso a <> "==")
+    | _ => false;
+
+fun bad_for_atp th = 
+  PureThy.is_internal th orelse too_complex (prop_of th) orelse is_strange_thm th;
+
 val multi_base_blacklist =
   ["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm"];
 
@@ -381,8 +390,7 @@
 
 (*Skolemize a named theorem, with Skolem functions as additional premises.*)
 fun skolem_thm (s,th) =
-  if (Sign.base_name s) mem_string multi_base_blacklist orelse 
-     PureThy.is_internal th orelse too_complex (prop_of th) then []
+  if (Sign.base_name s) mem_string multi_base_blacklist orelse bad_for_atp th then []
   else 
       let val ctxt0 = Variable.thm_context th
 	  val (nnfth,ctxt1) = to_nnf th ctxt0
@@ -450,8 +458,7 @@
 val mark_skolemized = Sign.add_consts_i [("ResAxioms_endtheory", HOLogic.boolT, NoSyn)];
 
 fun skolem_cache th thy =
-  if PureThy.is_internal th orelse too_complex (prop_of th) then thy
-  else #2 (skolem_cache_thm th thy);
+  if bad_for_atp th then thy else #2 (skolem_cache_thm th thy);
 
 fun skolem_cache_list (a,ths) thy =
   if (Sign.base_name a) mem_string multi_base_blacklist then thy
diff -r 6c3890cbceac -r 78f8aaa27493 src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Tue Oct 30 15:13:48 2007 +0100
+++ b/src/HOL/Tools/res_clause.ML	Tue Oct 30 15:28:53 2007 +0100
@@ -40,7 +40,6 @@
   val string_of_fol_type : fol_type -> string
   datatype type_literal = LTVar of string * string | LTFree of string * string
   exception CLAUSE of string * term
-  val isMeta : string -> bool
   val add_typs : typ list -> type_literal list
   val get_tvar_strs: typ list -> string list
   datatype arLit =
@@ -261,11 +260,6 @@
       let val (folTyps,ts) = ListPair.unzip (map type_of Ts)
       in (folTyps, union_all ts) end;
 
-
-(* Any variables created via the METAHYPS tactical should be treated as
-   universal vars, although it is represented as "Free(...)" by Isabelle *)
-val isMeta = String.isPrefix "METAHYP1_"
-
 (*Make literals for sorted type variables*)
 fun sorts_on_typs_aux (_, [])   = []
   | sorts_on_typs_aux ((x,i),  s::ss) =
diff -r 6c3890cbceac -r 78f8aaa27493 src/HOL/Tools/res_hol_clause.ML
--- a/src/HOL/Tools/res_hol_clause.ML	Tue Oct 30 15:13:48 2007 +0100
+++ b/src/HOL/Tools/res_hol_clause.ML	Tue Oct 30 15:28:53 2007 +0100
@@ -138,8 +138,7 @@
       in  (c',ts)  end
   | combterm_of thy (Free(v,t)) =
       let val (tp,ts) = type_of t
-          val v' = if RC.isMeta v then CombVar(RC.make_schematic_var(v,0),tp)
-                   else CombConst(RC.make_fixed_var v, tp, [])
+          val v' = CombConst(RC.make_fixed_var v, tp, [])
       in  (v',ts)  end
   | combterm_of thy (Var(v,t)) =
       let val (tp,ts) = type_of t