# HG changeset patch
# User mengj
# Date 1137728123 -3600
# Node ID 2d0af0574588d7fee0c0b920cfc667458c4d7c08
# Parent  cb6e0064c88cea5d04a7da615acd293ba01cb0ec
fixed a bug

diff -r cb6e0064c88c -r 2d0af0574588 src/HOL/Tools/res_hol_clause.ML
--- a/src/HOL/Tools/res_hol_clause.ML	Thu Jan 19 21:22:30 2006 +0100
+++ b/src/HOL/Tools/res_hol_clause.ML	Fri Jan 20 04:35:23 2006 +0100
@@ -330,33 +330,39 @@
   | simp_type_of (TFree (a,s)) = ResClause.mk_fol_type("Fixed",ResClause.make_fixed_type_var a,[])
   | simp_type_of (TVar (v,s)) = ResClause.mk_fol_type("Var",ResClause.make_schematic_type_var v,[]);
 
-
-
 fun comb_typ ("COMBI",t) = 
     let val t' = domain_type t
     in
 	[simp_type_of t']
     end
   | comb_typ ("COMBK",t) = 
-    let val (ab,_) = strip_type t
+    let val a = domain_type t
+	val b = domain_type (range_type t)
     in
-	map simp_type_of ab
+	map simp_type_of [a,b]
     end
   | comb_typ ("COMBS",t) = 
     let val t' = domain_type t
-	val ([a,b],c) = strip_type t' 
+	val a = domain_type t'
+	val b = domain_type (range_type t')
+	val c = range_type (range_type t')
     in 
 	map simp_type_of [a,b,c]
     end
   | comb_typ ("COMBB",t) = 
-    let val ([ab,ca,c],b) = strip_type t
+    let val ab = domain_type t
+	val ca = domain_type (range_type t)
 	val a = domain_type ab
+	val b = range_type ab
+	val c = domain_type ca
     in
 	map simp_type_of [a,b,c]
     end
   | comb_typ ("COMBC",t) =
     let val t1 = domain_type t
-	val ([a,b],c) = strip_type t1
+	val a = domain_type t1
+	val b = domain_type (range_type t1)
+	val c = range_type (range_type t1)
     in
 	map simp_type_of [a,b,c]
     end;