src/HOL/Tools/res_atp.ML
changeset 25761 466e714de2fc
parent 25492 4cc7976948ac
child 26278 f0c6839df608
     1.1 --- a/src/HOL/Tools/res_atp.ML	Wed Jan 02 12:22:05 2008 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Jan 02 12:22:38 2008 +0100
     1.3 @@ -829,6 +829,8 @@
     1.4                        their original "name hints" may be bad anyway.*)
     1.5      val thy = ProofContext.theory_of ctxt
     1.6    in
     1.7 +    if exists_type ResAxioms.type_has_empty_sort (prop_of goal)  
     1.8 +    then error "Proof state contains the empty sort" else ();
     1.9      Output.debug (fn () => "subgoals in isar_atp:\n" ^
    1.10                    Syntax.string_of_term ctxt (Logic.mk_conjunction_list (Thm.prems_of goal)));
    1.11      Output.debug (fn () => "current theory: " ^ Context.theory_name thy);