# HG changeset patch
# User paulson
# Date 1162222966 -3600
# Node ID 04d8e6eb9a2e116dbb06a046d7079171cea31570
# Parent  e69c0e82955a767ab1222c58d09a3cba877fca81
Purely cosmetic

diff -r e69c0e82955a -r 04d8e6eb9a2e src/HOL/Tools/res_hol_clause.ML
--- a/src/HOL/Tools/res_hol_clause.ML	Mon Oct 30 13:07:51 2006 +0100
+++ b/src/HOL/Tools/res_hol_clause.ML	Mon Oct 30 16:42:46 2006 +0100
@@ -23,10 +23,12 @@
 val equal_imp_fequal = thm "Reconstruction.equal_imp_fequal";
 
 
-(*A flag to set if we use extra combinators B',C',S', currently FALSE as the 5 standard
+(*A flag to set if we use the Turner optimizations. Currently FALSE, as the 5 standard
   combinators appear to work best.*)
-val use_combB'C'S' = ref false;
+val use_Turner = ref false;
 
+(*FIXME: these refs should probaby replaced by code to count the combinators in the 
+  translated form of the term.*)
 val combI_count = ref 0;
 val combK_count = ref 0;
 val combB_count = ref 0;
@@ -128,101 +130,102 @@
     end
   | mk_compact_comb tm _ _ = tm;
 
-fun compact_comb t Bnds count_comb = if !use_combB'C'S' then mk_compact_comb t Bnds count_comb else t;
+fun compact_comb t Bnds count_comb = 
+  if !use_Turner then mk_compact_comb t Bnds count_comb else t;
 
 fun lam2comb (Abs(x,tp,Bound 0)) _ count_comb = 
-    let val tpI = Type("fun",[tp,tp])
-	val _ = increI count_comb
-    in 
-	Const("Reconstruction.COMBI",tpI) 
-    end
+      let val tpI = Type("fun",[tp,tp])
+	  val _ = increI count_comb
+      in 
+	  Const("Reconstruction.COMBI",tpI) 
+      end
   | lam2comb (Abs(x,tp,Bound n)) Bnds count_comb = 
-    let val (Bound n') = decre_bndVar (Bound n)
-	val tb = List.nth(Bnds,n')
-	val tK = Type("fun",[tb,Type("fun",[tp,tb])])
-	val _ = increK count_comb 
-    in
-	Const("Reconstruction.COMBK",tK) $ (Bound n')
-    end
+      let val (Bound n') = decre_bndVar (Bound n)
+	  val tb = List.nth(Bnds,n')
+	  val tK = Type("fun",[tb,Type("fun",[tp,tb])])
+	  val _ = increK count_comb 
+      in
+	  Const("Reconstruction.COMBK",tK) $ (Bound n')
+      end
   | lam2comb (Abs(x,t1,Const(c,t2))) _ count_comb = 
-    let val tK = Type("fun",[t2,Type("fun",[t1,t2])])
-	val _ = increK count_comb 
-    in 
-	Const("Reconstruction.COMBK",tK) $ Const(c,t2) 
-    end
+      let val tK = Type("fun",[t2,Type("fun",[t1,t2])])
+	  val _ = increK count_comb 
+      in 
+	  Const("Reconstruction.COMBK",tK) $ Const(c,t2) 
+      end
   | lam2comb (Abs(x,t1,Free(v,t2))) _ count_comb =
-    let val tK = Type("fun",[t2,Type("fun",[t1,t2])])
-	val _ = increK count_comb
-    in
-	Const("Reconstruction.COMBK",tK) $ Free(v,t2)
-    end
+      let val tK = Type("fun",[t2,Type("fun",[t1,t2])])
+	  val _ = increK count_comb
+      in
+	  Const("Reconstruction.COMBK",tK) $ Free(v,t2)
+      end
   | lam2comb (Abs(x,t1,Var(ind,t2))) _ count_comb =
-    let val tK = Type("fun",[t2,Type("fun",[t1,t2])])
-	val _ = increK count_comb 
-    in
-	Const("Reconstruction.COMBK",tK) $ Var(ind,t2)
-    end
+      let val tK = Type("fun",[t2,Type("fun",[t1,t2])])
+	  val _ = increK count_comb 
+      in
+	  Const("Reconstruction.COMBK",tK) $ Var(ind,t2)
+      end
   | lam2comb (t as (Abs(x,t1,P$(Bound 0)))) Bnds count_comb =
-    let val nfreeP = not(is_free P 0)
-	val tr = Term.type_of1(t1::Bnds,P)
-    in
-	if nfreeP then (decre_bndVar P)
-	else (
-	      let val tI = Type("fun",[t1,t1])
-		  val P' = lam2comb (Abs(x,t1,P)) Bnds count_comb
-		  val tp' = Term.type_of1(Bnds,P')
-		  val tS = Type("fun",[tp',Type("fun",[tI,tr])])
-		  val _ = increI count_comb
-		  val _ = increS count_comb
-	      in
-		  compact_comb (Const("Reconstruction.COMBS",tS) $ P' $ Const("Reconstruction.COMBI",tI)) Bnds count_comb
-	      end)
-    end
+      let val nfreeP = not(is_free P 0)
+	  val tr = Term.type_of1(t1::Bnds,P)
+      in
+	  if nfreeP then (decre_bndVar P)
+	  else 
+	  let val tI = Type("fun",[t1,t1])
+	      val P' = lam2comb (Abs(x,t1,P)) Bnds count_comb
+	      val tp' = Term.type_of1(Bnds,P')
+	      val tS = Type("fun",[tp',Type("fun",[tI,tr])])
+	      val _ = increI count_comb
+	      val _ = increS count_comb
+	  in
+	      compact_comb (Const("Reconstruction.COMBS",tS) $ P' $ Const("Reconstruction.COMBI",tI)) Bnds count_comb
+	  end
+      end
 	    
   | lam2comb (t as (Abs(x,t1,P$Q))) Bnds count_comb =
-    let val (nfreeP,nfreeQ) = (not(is_free P 0),not(is_free Q 0))
-	val tpq = Term.type_of1(t1::Bnds, P$Q) 
-    in
-	if(nfreeP andalso nfreeQ) then (
+      let val nfreeP = not(is_free P 0)
+	  and nfreeQ = not(is_free Q 0)
+	  val tpq = Term.type_of1(t1::Bnds, P$Q) 
+      in
+	  if nfreeP andalso nfreeQ 
+	  then 
 	    let val tK = Type("fun",[tpq,Type("fun",[t1,tpq])])
 		val PQ' = decre_bndVar(P $ Q)
 		val _ = increK count_comb
 	    in 
 		Const("Reconstruction.COMBK",tK) $ PQ'
-	    end)
-	else (
-	      if nfreeP then (
-			       let val Q' = lam2comb (Abs(x,t1,Q)) Bnds count_comb
-				   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])])])
-				   val _ = increB count_comb
-			       in
-				   compact_comb (Const("Reconstruction.COMBB",tB) $ P' $ Q') Bnds count_comb 
-			       end)
-	      else (
-		    if nfreeQ then (
-				    let val P' = lam2comb (Abs(x,t1,P)) Bnds count_comb
-					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])])])
-					val _ = increC count_comb
-				    in
-					compact_comb (Const("Reconstruction.COMBC",tC) $ P' $ Q') Bnds count_comb
-				    end)
-		    else(
-			 let val P' = lam2comb (Abs(x,t1,P)) Bnds count_comb
-			     val Q' = lam2comb (Abs(x,t1,Q)) Bnds count_comb 
-			     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])])])
-			     val _ = increS count_comb
-			 in
-			     compact_comb (Const("Reconstruction.COMBS",tS) $ P' $ Q') Bnds count_comb
-			 end)))
-    end
+	    end
+	  else if nfreeP then 
+	    let val Q' = lam2comb (Abs(x,t1,Q)) Bnds count_comb
+		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])])])
+		val _ = increB count_comb
+	    in
+		compact_comb (Const("Reconstruction.COMBB",tB) $ P' $ Q') Bnds count_comb 
+	    end
+	  else if nfreeQ then 
+	    let val P' = lam2comb (Abs(x,t1,P)) Bnds count_comb
+		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])])])
+		val _ = increC count_comb
+	    in
+		compact_comb (Const("Reconstruction.COMBC",tC) $ P' $ Q') Bnds count_comb
+	    end
+          else
+	    let val P' = lam2comb (Abs(x,t1,P)) Bnds count_comb
+		val Q' = lam2comb (Abs(x,t1,Q)) Bnds count_comb 
+		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])])])
+		val _ = increS count_comb
+	    in
+		compact_comb (Const("Reconstruction.COMBS",tS) $ P' $ Q') Bnds count_comb
+	    end
+      end
   | lam2comb (t as (Abs(x,t1,_))) _ _ = raise ResClause.CLAUSE("HOL CLAUSE",t);
 
 (*********************)