From d9154d00af630841b23998fbef36b92b45eb467b Mon Sep 17 00:00:00 2001
From: Matthew Fernandez <matthew.fernandez@nicta.com.au>
Date: Wed, 25 Nov 2015 10:29:22 +1100
Subject: [PATCH] crefine: Remove a find_theorems invocation.

---
 proof/crefine/Retype_C.thy | 2 --
 1 file changed, 2 deletions(-)

diff --git a/proof/crefine/Retype_C.thy b/proof/crefine/Retype_C.thy
index 3d866af40..90aa4a579 100644
--- a/proof/crefine/Retype_C.thy
+++ b/proof/crefine/Retype_C.thy
@@ -790,8 +790,6 @@ lemma list_map_length_is_None [simp]:
   apply (simp add: list_map_def)
   done
 
-find_theorems h_t_valid intvl
-
 lemma list_map_append_one:
   "list_map (xs @ [x]) = [length xs \<mapsto> x] ++ list_map xs"
   by (simp add: list_map_def)