equal
deleted
inserted
replaced
225 ((map snd ls) @ [dummyT]) |
225 ((map snd ls) @ [dummyT]) |
226 (list_comb (Const (rec_name, dummyT), |
226 (list_comb (Const (rec_name, dummyT), |
227 fs @ map Bound (0 ::(length ls downto 1)))) |
227 fs @ map Bound (0 ::(length ls downto 1)))) |
228 val def_name = Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def"; |
228 val def_name = Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def"; |
229 val def_prop = |
229 val def_prop = |
230 singleton (ProofContext.infer_types (ProofContext.init thy)) |
230 singleton (Syntax.check_terms (ProofContext.init thy)) |
231 (Logic.mk_equals (Const (fname, dummyT), rhs)); |
231 (Logic.mk_equals (Const (fname, dummyT), rhs)); |
232 in (def_name, def_prop) end; |
232 in (def_name, def_prop) end; |
233 |
233 |
234 |
234 |
235 (* find datatypes which contain all datatypes in tnames' *) |
235 (* find datatypes which contain all datatypes in tnames' *) |