--- a/src/HOL/List.thy Fri Sep 27 09:26:31 2013 +0200
+++ b/src/HOL/List.thy Fri Sep 27 10:40:02 2013 +0200
@@ -6002,7 +6002,8 @@
lemma equal_Nil_null [code_unfold]:
"HOL.equal xs [] \<longleftrightarrow> null xs"
- by (simp add: equal eq_Nil_null)
+ "HOL.equal [] = null"
+ by (auto simp add: equal null_def)
definition maps :: "('a \<Rightarrow> 'b list) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
[code_abbrev]: "maps f xs = concat (map f xs)"
--- a/src/HOL/Option.thy Fri Sep 27 09:26:31 2013 +0200
+++ b/src/HOL/Option.thy Fri Sep 27 10:40:02 2013 +0200
@@ -187,7 +187,8 @@
lemma [code_unfold]:
"HOL.equal x None \<longleftrightarrow> is_none x"
- by (simp add: equal is_none_def)
+ "HOL.equal None = is_none"
+ by (auto simp add: equal is_none_def)
hide_const (open) is_none
--- a/src/Pure/item_net.ML Fri Sep 27 09:26:31 2013 +0200
+++ b/src/Pure/item_net.ML Fri Sep 27 10:40:02 2013 +0200
@@ -12,6 +12,7 @@
val content: 'a T -> 'a list
val length: 'a T -> int
val retrieve: 'a T -> term -> 'a list
+ val retrieve_matching: 'a T -> term -> 'a list
val member: 'a T -> 'a -> bool
val merge: 'a T * 'a T -> 'a T
val remove: 'a -> 'a T -> 'a T
@@ -39,6 +40,7 @@
fun content (Items {content, ...}) = content;
fun length items = List.length (content items);
fun retrieve (Items {net, ...}) = order_list o Net.unify_term net;
+fun retrieve_matching (Items {net, ...}) = order_list o Net.match_term net;
(* standard operations *)