237 |
237 |
238 |
238 |
239 fun instantiate_types thy t = |
239 fun instantiate_types thy t = |
240 let val sg = sign_of thy |
240 let val sg = sign_of thy |
241 val rsg = Sign.rep_sg sg |
241 val rsg = Sign.rep_sg sg |
242 in fst(Type.infer_types(#tsig rsg, lookup_const sg, K None, K None, |
242 in fst(Type.infer_types(#tsig rsg, Sign.const_type sg, K None, K None, |
243 TVar(("",0),[]), t)) |
243 TVar(("",0),[]), t)) |
244 end; |
244 end; |
245 |
245 |
246 in |
246 in |
247 fun add_datatype (typevars, tname, cons_list') thy = |
247 fun add_datatype (typevars, tname, cons_list') thy = |
533 , fns @ map Bound (0 ::(length ls downto 1)))); |
533 , fns @ map Bound (0 ::(length ls downto 1)))); |
534 val sg = sign_of thy; |
534 val sg = sign_of thy; |
535 val (defname,def) = mk_defpair (Const(fname,dummyT),rhs) |
535 val (defname,def) = mk_defpair (Const(fname,dummyT),rhs) |
536 val tdef as ( _ $ Const(_,T) $ _ ) = instantiate_types thy def; |
536 val tdef as ( _ $ Const(_,T) $ _ ) = instantiate_types thy def; |
537 val varT = Type.varifyT T; |
537 val varT = Type.varifyT T; |
538 val Some(ftyp) = lookup_const sg fname; |
538 val Some(ftyp) = Sign.const_type sg fname; |
539 in |
539 in |
540 if Type.typ_instance (#tsig(Sign.rep_sg sg), ftyp, varT) |
540 if Type.typ_instance (#tsig(Sign.rep_sg sg), ftyp, varT) |
541 then add_defs_i [(defname,tdef)] thy |
541 then add_defs_i [(defname,tdef)] thy |
542 else error("Primrec definition error: \ntype of " ^ fname |
542 else error("Primrec definition error: \ntype of " ^ fname |
543 ^ " is not instance of type deduced from equations") |
543 ^ " is not instance of type deduced from equations") |