--- 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;
-