# HG changeset patch
# User Andreas Lochbihler
# Date 1380271202 -7200
# Node ID 54b08afc03c762706e9d04f1552cee9448a6795f
# Parent  5431e1392b142d1564f5543f963b3afb2d49fb1b# Parent  fc631b2831d30f7376156040b88a15fd005f785c
merged

diff -r 5431e1392b14 -r 54b08afc03c7 src/HOL/List.thy
--- 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)"
diff -r 5431e1392b14 -r 54b08afc03c7 src/HOL/Option.thy
--- 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
 
diff -r 5431e1392b14 -r 54b08afc03c7 src/Pure/item_net.ML
--- 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 *)