src/HOL/Quickcheck_Narrowing.thy

 
 instance ..
 
 end
 
-lemma [code, code del]: "partial_term_of (ty :: int itself) t \<equiv> undefined"
-  by (rule partial_term_of_anything)+
+declare [[code drop: "partial_term_of :: int itself \<Rightarrow> _"]]
 
 lemma [code]:
   "partial_term_of (ty :: int itself) (Narrowing_variable p t) \<equiv>
     Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Int.int'') [])"
   "partial_term_of (ty :: int itself) (Narrowing_constructor i []) \<equiv>

 
 instance ..
 
 end
 
-lemma [code, code del]: "partial_term_of (ty :: integer itself) t \<equiv> undefined"
-  by (rule partial_term_of_anything)+
+declare [[code drop: "partial_term_of :: integer itself \<Rightarrow> _"]]  
 
 lemma [code]:
   "partial_term_of (ty :: integer itself) (Narrowing_variable p t) \<equiv>
     Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Code_Numeral.integer'') [])"
   "partial_term_of (ty :: integer itself) (Narrowing_constructor i []) \<equiv>