diff -r 85f62d491ff7 -r 8ff6c8c95870 datatype.ML
--- a/datatype.ML	Mon Sep 26 18:04:43 1994 +0100
+++ b/datatype.ML	Tue Sep 27 13:23:04 1994 +0100
@@ -522,13 +522,13 @@
 	     ,list_comb(rec_comb
 			, fns @ map Bound (0 ::(length ls downto 1))));
           val sg = sign_of thy;
-          val defpair as (defname,_) =  mk_defpair (Const(fname,dummyT),rhs)
-	  val (_,tdef as ( _ $ Const(_,T) $ _ )) = inferT_axm sg defpair;
+          val defpair =  mk_defpair (Const(fname,dummyT),rhs)
+	  val defpairT as (_, _ $ Const(_,T) $ _ ) = inferT_axm sg defpair;
 	  val varT = Type.varifyT T;
           val Some(ftyp) = Sign.const_type sg fname;
 	in
 	  if Type.typ_instance (#tsig(Sign.rep_sg sg), ftyp, varT)
-	  then add_defs_i [(defname,tdef)] thy
+	  then add_defs_i [defpairT] thy
 	  else error("Primrec definition error: \ntype of " ^ fname 
 		     ^ " is not instance of type deduced from equations")
 	end;
@@ -543,4 +543,3 @@
     end
 end
 end;
-