equal
deleted
inserted
replaced
136 val absrep_trm = (fold_rev mk_fun_map rep_fns abs_fn $ rhs) |
136 val absrep_trm = (fold_rev mk_fun_map rep_fns abs_fn $ rhs) |
137 |> Syntax.check_term lthy |
137 |> Syntax.check_term lthy |
138 |
138 |
139 val ((trm, thm), lthy') = define nconst_bname mx attr absrep_trm lthy |
139 val ((trm, thm), lthy') = define nconst_bname mx attr absrep_trm lthy |
140 |
140 |
141 val nconst_str = Binding.str_of nconst_bname |
141 val nconst_str = Binding.name_of nconst_bname |
142 val qc_info = {qconst = trm, rconst = rhs} |
142 val qc_info = {qconst = trm, rconst = rhs} |
143 val lthy'' = qconsts_update nconst_str qc_info lthy' |
143 val lthy'' = qconsts_update nconst_str qc_info lthy' |
144 in |
144 in |
145 ((trm, thm), lthy'') |
145 ((trm, thm), lthy'') |
146 end |
146 end |