src/HOL/List.thy
changeset 41075 4bed56dc95fb
parent 40968 a6fcd305f7dc
child 41229 d797baa3d57c
--- a/src/HOL/List.thy	Wed Dec 08 13:34:50 2010 +0100
+++ b/src/HOL/List.thy	Wed Dec 08 13:34:50 2010 +0100
@@ -4217,7 +4217,7 @@
   show "inf (listsp A) (listsp B) \<le> listsp (inf A B)" by (blast intro!: listsp_infI predicate1I)
 qed
 
-lemmas listsp_conj_eq [simp] = listsp_inf_eq [simplified inf_fun_eq inf_bool_eq]
+lemmas listsp_conj_eq [simp] = listsp_inf_eq [simplified inf_fun_def inf_bool_def]
 
 lemmas lists_Int_eq [simp] = listsp_inf_eq [to_set pred_equals_eq]