equal
deleted
inserted
replaced
87 |
87 |
88 |
88 |
89 (* prepare_typedef *) |
89 (* prepare_typedef *) |
90 |
90 |
91 fun read_term sg used s = |
91 fun read_term sg used s = |
92 #1 (Thm.read_def_cterm (sg, K None, K None) used true (s, HOLogic.termTVar)); |
92 #1 (Thm.read_def_cterm (sg, K None, K None) used true (s, HOLogic.termT)); |
93 |
93 |
94 fun cert_term sg _ t = Thm.cterm_of sg t handle TERM (msg, _) => error msg; |
94 fun cert_term sg _ t = Thm.cterm_of sg t handle TERM (msg, _) => error msg; |
95 |
95 |
96 fun err_in_typedef name = |
96 fun err_in_typedef name = |
97 error ("The error(s) above occurred in typedef " ^ quote name); |
97 error ("The error(s) above occurred in typedef " ^ quote name); |