src/HOL/Quickcheck_Narrowing.thy
changeset 68484 59793df7f853
parent 67399 eab6ce8368fa
child 69528 9d0e492e3229
--- a/src/HOL/Quickcheck_Narrowing.thy	Fri Jun 22 18:31:50 2018 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy	Fri Jun 22 20:31:49 2018 +0200
@@ -54,7 +54,7 @@
 where
   "map_cons f (Narrowing_cons ty cs) = Narrowing_cons ty (map (\<lambda>c. f \<circ> c) cs)"
 
-subsubsection \<open>From narrowing's deep representation of terms to @{theory Code_Evaluation}'s terms\<close>
+subsubsection \<open>From narrowing's deep representation of terms to @{theory HOL.Code_Evaluation}'s terms\<close>
 
 class partial_term_of = typerep +
   fixes partial_term_of :: "'a itself => narrowing_term => Code_Evaluation.term"