changeset 59621 | 291934bac95e |
parent 59582 | 0fbed69ff081 |
child 59936 | b8ffc3dc9e24 |
--- a/src/HOL/Nominal/nominal_primrec.ML Fri Mar 06 14:01:08 2015 +0100 +++ b/src/HOL/Nominal/nominal_primrec.ML Fri Mar 06 15:58:56 2015 +0100 @@ -281,7 +281,7 @@ val qualify = Binding.qualify false (space_implode "_" (map (Long_Name.base_name o #1) defs)); val names_atts' = map (apfst qualify) names_atts; - val cert = Proof_Context.cterm_of lthy'; + val cert = Thm.cterm_of lthy'; fun mk_idx eq = let