--- a/src/HOL/Quickcheck_Narrowing.thy Tue Jun 20 13:07:45 2017 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy Tue Jun 20 13:07:47 2017 +0200
@@ -260,8 +260,7 @@
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>
@@ -283,8 +282,7 @@
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>