quotient_def.ML
changeset 312 4cf79f70efec
parent 310 fec6301a1989
child 318 746b17e1d6d8
equal deleted inserted replaced
311:77fc6f3c0343 312:4cf79f70efec
   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