| changeset 53815 | e8aa538e959e |
| parent 53806 | de4653037e0d |
| child 54294 | 98826791a588 |
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Sep 24 09:12:09 2013 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Sep 24 11:02:42 2013 +0200 @@ -629,7 +629,6 @@ fun register_codatatype_generic co_T case_name constr_xs generic = let - val ctxt = Context.proof_of generic val thy = Context.theory_of generic val {frac_types, ersatz_table, codatatypes} = Data.get generic val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs