# HG changeset patch
# User paulson
# Date 835953187 -7200
# Node ID 861e29c7cadacb65aae76c4da31a521e241f38e7
# Parent  07eee14f5bd4bcf5a8f1b49f411d337d1f3601ae
Added type-checking to rule "combination".  This corrects a fault
concerning soundness.  See Jeremy Dawsons message of 27 Jun 1996 on
isabelle-users

diff -r 07eee14f5bd4 -r 861e29c7cada src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Jun 28 11:10:32 1996 +0200
+++ b/src/Pure/thm.ML	Fri Jun 28 11:13:07 1996 +0200
@@ -833,15 +833,24 @@
 	      prop=prop1,...} = th1
       and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, 
 	      prop=prop2,...} = th2
+      fun chktypes (f,t) =
+	    (case fastype_of f of
+		Type("fun",[T1,T2]) => 
+		    if T1 <> fastype_of t then
+			 raise THM("combination: types", 0, [th1,th2])
+		    else ()
+		| _ => raise THM("combination: not function type", 0, 
+				 [th1,th2]))
   in case (prop1,prop2)  of
        (Const("==",_) $ f $ g, Const("==",_) $ t $ u) =>
-          let val thm = (*no fix_shyps*)
-             Thm{sign = merge_thm_sgs(th1,th2), 
-		 der = infer_derivs (Combination, [der1, der2]),
-                 maxidx = max[max1,max2], 
-		 shyps = shyps1 union shyps2,
-                 hyps = hyps1 union hyps2,
-		 prop = Logic.mk_equals(f$t, g$u)}
+          let val _   = chktypes (f,t)
+	      val thm = (*no fix_shyps*)
+			Thm{sign = merge_thm_sgs(th1,th2), 
+			    der = infer_derivs (Combination, [der1, der2]),
+			    maxidx = max[max1,max2], 
+			    shyps = shyps1 union shyps2,
+			    hyps = hyps1 union hyps2,
+			    prop = Logic.mk_equals(f$t, g$u)}
           in nodup_Vars thm "combination"; thm end
      | _ =>  raise THM("combination: premises", 0, [th1,th2])
   end;