src/HOL/Tools/res_hol_clause.ML

 structure ResHolClause =
 
 struct
 
 
+val include_combS = ref false;
+val include_min_comb = ref false;
 
 
 (**********************************************************************)
 (* convert a Term.term with lambdas into a Term.term with combinators *) 
 (**********************************************************************)

 
 (*******************************************)
 fun lam2comb (Abs(x,tp,Bound 0)) _ = 
     let val tpI = Type("fun",[tp,tp])
     in 
+	include_min_comb:=true;
 	Const("COMBI",tpI) 
     end
   | lam2comb (Abs(x,t1,Const(c,t2))) _ = 
     let val tK = Type("fun",[t2,Type("fun",[t1,t2])])
     in 
+	include_min_comb:=true;
 	Const("COMBK",tK) $ Const(c,t2) 
     end
   | lam2comb (Abs(x,t1,Free(v,t2))) _ =
     let val tK = Type("fun",[t2,Type("fun",[t1,t2])])
     in
+	include_min_comb:=true;
 	Const("COMBK",tK) $ Free(v,t2)
     end
   | lam2comb (Abs(x,t1,Var(ind,t2))) _=
     let val tK = Type("fun",[t2,Type("fun",[t1,t2])])
     in
+	include_min_comb:=true;
 	Const("COMBK",tK) $ Var(ind,t2)
     end
   | lam2comb (t as (Abs(x,t1,P$(Bound 0)))) Bnds =
     let val nfreeP = not(is_free P 0)
 	val tr = Term.type_of1(t1::Bnds,P)

 	      let val tI = Type("fun",[t1,t1])
 		  val P' = lam2comb (Abs(x,t1,P)) Bnds
 		  val tp' = Term.type_of1(Bnds,P')
 		  val tS = Type("fun",[tp',Type("fun",[tI,tr])])
 	      in
+		  include_min_comb:=true;
+		  include_combS:=true;
 		  Const("COMBS",tS) $ P' $ Const("COMBI",tI)
 	      end)
     end
 	    
   | lam2comb (t as (Abs(x,t1,P$Q))) Bnds =

     in
 	if(nfreeP andalso nfreeQ) then (
 	    let val tK = Type("fun",[tpq,Type("fun",[t1,tpq])])
 		val PQ' = decre_bndVar(P $ Q)
 	    in 
+		include_min_comb:=true;
 		Const("COMBK",tK) $ PQ'
 	    end)
 	else (
 	      if nfreeP then (
 			       let val Q' = lam2comb (Abs(x,t1,Q)) Bnds
 				   val P' = decre_bndVar P
 				   val tp = Term.type_of1(Bnds,P')
 				   val tq' = Term.type_of1(Bnds, Q')
 				   val tB = Type("fun",[tp,Type("fun",[tq',Type("fun",[t1,tpq])])])
 			       in
+				   include_min_comb:=true;
 				   Const("COMBB",tB) $ P' $ Q' 
 			       end)
 	      else (
 		    if nfreeQ then (
 				    let val P' = lam2comb (Abs(x,t1,P)) Bnds
 					val Q' = decre_bndVar Q
 					val tq = Term.type_of1(Bnds,Q')
 					val tp' = Term.type_of1(Bnds, P')
 					val tC = Type("fun",[tp',Type("fun",[tq,Type("fun",[t1,tpq])])])
 				    in
+					include_min_comb:=true;
 					Const("COMBC",tC) $ P' $ Q'
 				    end)
 		    else(
 			 let val P' = lam2comb (Abs(x,t1,P)) Bnds
 			     val Q' = lam2comb (Abs(x,t1,Q)) Bnds
 			     val tp' = Term.type_of1(Bnds,P')
 			     val tq' = Term.type_of1(Bnds,Q')
 			     val tS = Type("fun",[tp',Type("fun",[tq',Type("fun",[t1,tpq])])])
 			 in
+			     include_min_comb:=true;
+			     include_combS:=true;
 			     Const("COMBS",tS) $ P' $ Q'
 			 end)))
     end
   | lam2comb (t as (Abs(x,t1,_))) _ = raise LAM2COMB (t);
 

 
 (*********************************************************************)
 (* convert a clause with type Term.term to a clause with type clause *)
 (*********************************************************************)
 
-
 fun isFalse (Literal(pol,Bool(CombConst(c,_)))) =
     (pol andalso c = "c_False") orelse
     (not pol andalso c = "c_True")
   | isFalse _ = false;
 

 (* convert clause into ATP specific formats:                          *)
 (* TPTP used by Vampire and E                                         *)
 (**********************************************************************)
 
 val keep_types = ref true;
-val include_combS = ref false;
-
 
 val type_wrapper = "typeinfo";
 
 fun put_type (c,t) = 
     if !keep_types then type_wrapper ^ (ResClause.paren_pack [c,t])