89 

    89 

    90   val ((trm, thm), lthy') = define qconst_bname mx attr newrhs lthy

    90   val ((trm, thm), lthy') = define qconst_bname mx attr newrhs lthy

    91 

    91 

    92   fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs, def = thm}

    92   fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs, def = thm}

    93   val lthy'' = Local_Theory.declaration true

    93   val lthy'' = Local_Theory.declaration true

    95                  (fn phi => 

    94                  (fn phi => 

    96                        let

    95                        let

    97                          val qconst_str = Binding.name_of qconst_bname

    96                          val qconst_str = Binding.name_of qconst_bname

    98                        in                      

    97                        in                      

    99                          qconsts_update_gen qconst_str (qcinfo phi)

    98                          qconsts_update_gen qconst_str (qcinfo phi)