equal
deleted
inserted
replaced
70 val ((trm, (_ , thm)), lthy') = Local_Theory.define (var, (attr, newrhs)) lthy |
70 val ((trm, (_ , thm)), lthy') = Local_Theory.define (var, (attr, newrhs)) lthy |
71 |
71 |
72 (* data storage *) |
72 (* data storage *) |
73 val qconst_data = {qconst = trm, rconst = rhs, def = thm} |
73 val qconst_data = {qconst = trm, rconst = rhs, def = thm} |
74 |
74 |
75 fun qcinfo phi = Quotient_Info.transform_quotconsts phi qconst_data |
75 val lthy'' = lthy' |
76 fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi) |
76 |> Local_Theory.declaration {syntax = false, pervasive = true} |
77 val lthy'' = |
77 (fn phi => |
78 Local_Theory.declaration {syntax = false, pervasive = true} |
78 (case Quotient_Info.transform_quotconsts phi qconst_data of |
79 (fn phi => Quotient_Info.update_quotconsts (trans_name phi) (qcinfo phi)) lthy' |
79 qcinfo as {qconst = Const (c, _), ...} => |
|
80 Quotient_Info.update_quotconsts c qcinfo |
|
81 | _ => I)); |
80 in |
82 in |
81 (qconst_data, lthy'') |
83 (qconst_data, lthy'') |
82 end |
84 end |
83 |
85 |
84 fun check_term' cnstr ctxt = |
86 fun check_term' cnstr ctxt = |