equal
deleted
inserted
replaced
133 fun mk_fun_map t s = |
133 fun mk_fun_map t s = |
134 Const (@{const_name "fun_map"}, dummyT) $ t $ s |
134 Const (@{const_name "fun_map"}, dummyT) $ t $ s |
135 |
135 |
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 |
|
139 val ((trm, thm), lthy') = define nconst_bname mx attr absrep_trm lthy |
|
140 |
|
141 val nconst_str = Binding.str_of nconst_bname |
|
142 val qc_info = {qconst = trm, rconst = rhs} |
|
143 val lthy'' = qconsts_update nconst_str qc_info lthy' |
138 in |
144 in |
139 define nconst_bname mx attr absrep_trm lthy |
145 ((trm, thm), lthy'') |
140 end |
146 end |
141 |
147 |
142 (* interface and syntax setup *) |
148 (* interface and syntax setup *) |
143 |
149 |
144 (* the ML-interface takes a 5-tuple consisting of *) |
150 (* the ML-interface takes a 5-tuple consisting of *) |