src/HOL/Tools/res_atp.ML
changeset 25243 78f8aaa27493
parent 25085 aa9db4e3cd5e
child 25492 4cc7976948ac
     1.1 --- a/src/HOL/Tools/res_atp.ML	Tue Oct 30 15:13:48 2007 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Oct 30 15:28:53 2007 +0100
     1.3 @@ -468,8 +468,8 @@
     1.4          val xname = NameSpace.extern space name;
     1.5        in
     1.6          if blacklisted name then I
     1.7 -        else if is_valid (xname, ths) then cons (xname, ths)
     1.8 -        else if is_valid (name, ths) then cons (name, ths)
     1.9 +        else if is_valid (xname, ths) then cons (xname, filter_out ResAxioms.bad_for_atp ths)
    1.10 +        else if is_valid (name, ths) then cons (name, filter_out ResAxioms.bad_for_atp ths)
    1.11          else I
    1.12        end;
    1.13      val thy = ProofContext.theory_of ctxt;
    1.14 @@ -731,6 +731,8 @@
    1.15          | get_neg_subgoals (gl::gls) n = #1 (ResAxioms.neg_conjecture_clauses th n) ::
    1.16                                           get_neg_subgoals gls (n+1)
    1.17        val goal_cls = get_neg_subgoals goals 1
    1.18 +                     handle THM ("assume: variables", _, _) => 
    1.19 +                       error "Sledgehammer: Goal contains type variables (TVars)"                       
    1.20        val isFO = case !linkup_logic_mode of
    1.21  			  Auto => forall (Meson.is_fol_term thy) (map prop_of (List.concat goal_cls))
    1.22  			| Fol => true