changeset 59580 | cbc38731d42f |
parent 58956 | a816aa3ff391 |
child 59582 | 0fbed69ff081 |
--- a/src/HOL/Nominal/nominal_primrec.ML Tue Mar 03 17:20:51 2015 +0100 +++ b/src/HOL/Nominal/nominal_primrec.ML Tue Mar 03 19:08:04 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 = cterm_of (Proof_Context.theory_of lthy'); + val cert = Proof_Context.cterm_of lthy'; fun mk_idx eq = let