equal
deleted
inserted
replaced
94 val absrep_trm = (fold_rev mk_fun_map rep_fns abs_fn $ rhs) |
94 val absrep_trm = (fold_rev mk_fun_map rep_fns abs_fn $ rhs) |
95 |> Syntax.check_term lthy |
95 |> Syntax.check_term lthy |
96 |
96 |
97 val ((trm, thm), lthy') = define qconst_bname mx attr absrep_trm lthy |
97 val ((trm, thm), lthy') = define qconst_bname mx attr absrep_trm lthy |
98 |
98 |
99 val qconst_str = Binding.name_of qconst_bname |
|
100 fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs, def = thm} |
99 fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs, def = thm} |
101 val lthy'' = Local_Theory.declaration true |
100 val lthy'' = Local_Theory.declaration true |
102 (fn phi => qconsts_update_gen qconst_str (qcinfo phi)) lthy' |
101 (fn phi => |
|
102 let |
|
103 val qconst_str = fst (Term.dest_Const (Morphism.term phi trm)) |
|
104 in |
|
105 qconsts_update_gen qconst_str (qcinfo phi) |
|
106 end) lthy' |
103 in |
107 in |
104 ((trm, thm), lthy'') |
108 ((trm, thm), lthy'') |
105 end |
109 end |
106 |
110 |
107 (* interface and syntax setup *) |
111 (* interface and syntax setup *) |