Perform higher-order pattern matching during round-up.

--- a/src/FOL/ex/NewLocaleTest.thy	Thu Nov 27 21:25:34 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy	Fri Nov 28 11:14:13 2008 +0100
@@ -217,9 +217,47 @@
 print_locale! lgrp
 
 
+(* Duality *)
+
+locale order =
+  fixes less :: "'a => 'a => o" (infix "<<" 50)
+  assumes refl: "x << x"
+    and trans: "[| x << y; y << z |] ==> x << z"
+
+sublocale order < dual: order "%x y. y << x"
+  apply (rule order.intro) apply (rule refl) apply (blast intro: trans)
+  done
+
+print_locale! order  (* Only two instances of order. *)
+
+locale order' =
+  fixes less :: "'a => 'a => o" (infix "<<" 50)
+  assumes refl: "x << x"
+    and trans: "[| x << y; y << z |] ==> x << z"
+
+locale order_with_def = order'
+begin
+
+definition greater :: "'a => 'a => o" (infix ">>" 50) where
+  "x >> y <-> y << x"
+
+end
+
+sublocale order_with_def < dual: order' "op >>"
+  apply (intro order'.intro)
+  unfolding greater_def
+  apply (rule refl) apply (blast intro: trans)
+  done
+
+print_locale! order_with_def
+(* Note that decls come after theorems that make use of them.
+  Appears to be harmless at least in this example. *)
+
+
 (* locale with many parameters ---
    interpretations generate alternating group A5 *)
 
+
 locale A5 =
   fixes A and B and C and D and E
   assumes eq: "A <-> B <-> C <-> D <-> E"
@@ -259,4 +297,9 @@
 
 context trivial begin thm x.Q [where ?x = True] end
 
+sublocale trivial < y: trivial Q Q
+  apply (intro trivial.intro) using Q by fast
+
+print_locale! trivial  (* No instance for y created (subsumed). *)
+
 end

--- a/src/Pure/Isar/new_locale.ML	Thu Nov 27 21:25:34 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML	Fri Nov 28 11:14:13 2008 +0100
@@ -162,21 +162,16 @@
 
 (** Resolve locale dependencies in a depth-first fashion **)
 
+type identifiers = (string * term list) list;
+
+val empty = ([] : identifiers);
+
 local
 
-structure Idtab = TableFun(type key = string * term list
-  val ord = prod_ord string_ord (list_ord Term.fast_term_ord));
-
-in
-
-type identifiers = unit Idtab.table
-
-val empty = (Idtab.empty : identifiers);
+fun ident_eq thy ((n, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
 
 val roundup_bound = 120;
 
-local
-
 fun add thy depth (name, morph) (deps, marked) =
   if depth > roundup_bound
   then error "Roundup bound exceeded (sublocale relation probably not terminating)."
@@ -186,13 +181,13 @@
       val instance = params |>
         map ((fn (b, T, _) => Free (Name.name_of b, the T)) #> Morphism.term morph);
     in
-      if Idtab.defined marked (name, instance)
+      if member (ident_eq thy) marked (name, instance)
       then (deps, marked)
       else
         let
           val dependencies' =
             map (fn ((name, morph'), _) => (name, morph' $>  morph)) dependencies;
-          val marked' = Idtab.insert (op =) ((name, instance), ()) marked;
+          val marked' = (name, instance) :: marked;
           val (deps', marked'') = fold_rev (add thy (depth + 1)) dependencies' ([], marked');
         in
           ((name, morph) :: deps' @ deps, marked'')
@@ -212,8 +207,6 @@
 
 end;
 
-end;
-
 
 (* Declarations and facts *)