simplification of locale interfaces

--- a/src/Pure/Isar/class_target.ML	Wed Jul 15 10:11:13 2009 +0200
+++ b/src/Pure/Isar/class_target.ML	Wed Jul 15 18:20:08 2009 +0200
@@ -242,15 +242,16 @@
     val diff_sort = Sign.complete_sort thy [sup]
       |> subtract (op =) (Sign.complete_sort thy [sub])
       |> filter (is_class thy);
-    val deps_witss = case some_dep_morph
-     of SOME dep_morph => [((sup, dep_morph), the_list some_wit)]
-      | NONE => []
+    val add_dependency = case some_dep_morph
+     of SOME dep_morph => Locale.add_dependency sub
+          (sup, dep_morph $> Element.satisfy_morphism (the_list some_wit)) export
+      | NONE => I
   in
     thy
     |> AxClass.add_classrel classrel
     |> ClassData.map (Graph.add_edge (sub, sup))
     |> activate_defs sub (these_defs thy diff_sort)
-    |> Locale.add_dependencies sub deps_witss export
+    |> add_dependency
   end;
 
 

--- a/src/Pure/Isar/expression.ML	Wed Jul 15 10:11:13 2009 +0200
+++ b/src/Pure/Isar/expression.ML	Wed Jul 15 18:20:08 2009 +0200
@@ -788,27 +788,6 @@
 
 (*** Interpretation ***)
 
-(** Interpretation between locales: declaring sublocale relationships **)
-
-local
-
-fun gen_sublocale prep_expr intern raw_target expression thy =
-  let
-    val target = intern thy raw_target;
-    val target_ctxt = Locale.init target thy;
-    val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
-    fun after_qed witss = ProofContext.theory
-      (Locale.add_dependencies target (deps ~~ witss) export);
-  in Element.witness_proof after_qed propss goal_ctxt end;
-
-in
-
-fun sublocale x = gen_sublocale cert_goal_expression (K I) x;
-fun sublocale_cmd x = gen_sublocale read_goal_expression Locale.intern x;
-
-end;
-
-
 (** Interpretation in theories **)
 
 local
@@ -816,46 +795,31 @@
 fun gen_interpretation prep_expr parse_prop prep_attr
     expression equations theory =
   let
-    val ((propss, regs, export), expr_ctxt) = ProofContext.init theory
+    val ((propss, deps, export), expr_ctxt) = ProofContext.init theory
       |> prep_expr expression;
 
     val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
-    val eq_attns = map ((apsnd o map) (prep_attr theory) o fst) equations;
+    val attrss = map ((apsnd o map) (prep_attr theory) o fst) equations;
     val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
     val export' = Variable.export_morphism goal_ctxt expr_ctxt;
 
-    fun store_reg ((name, morph), wits) thy =
+    fun note_eqns raw_eqns thy =
       let
-        val wits' = map (Element.morph_witness export') wits;
-        val morph' = morph $> Element.satisfy_morphism wits';
+        val eqns = map (Morphism.thm (export' $> export)) raw_eqns;
+        val eqn_attrss = map2 (fn attrs => fn eqn =>
+          ((apsnd o map) (Attrib.attribute_i thy) attrs, [([eqn], [])])) attrss eqns;
+        fun meta_rewrite thy = map (LocalDefs.meta_rewrite_rule (ProofContext.init thy) #>
+          Drule.abs_def) o maps snd;
       in
         thy
-        |> Locale.add_registration (name, (morph', export))
-        |> pair (name, morph')
+        |> PureThy.note_thmss Thm.lemmaK eqn_attrss
+        |-> (fn facts => `(fn thy => meta_rewrite thy facts))
       end;
 
-    fun store_eqns_activate regs [] thy =
-          thy
-          |> fold (fn (name, morph) =>
-               Context.theory_map (Locale.activate_facts (name, morph $> export))) regs
-      | store_eqns_activate regs eqs thy =
-          let
-            val eqs' = eqs |> map (Morphism.thm (export' $> export));
-            val morph_eqs = eqs' |> map (LocalDefs.meta_rewrite_rule (ProofContext.init thy) #>
-              Drule.abs_def);
-            val eq_morph = Element.eq_morphism thy morph_eqs;
-            val eq_attns' = map ((apsnd o map) (Attrib.attribute_i thy)) eq_attns;
-          in
-            thy
-            |> fold (fn (name, morph) =>
-                Locale.amend_registration eq_morph (name, morph) #>
-                Context.theory_map (Locale.activate_facts (name, morph $> eq_morph $> export))) regs
-            |> PureThy.note_thmss Thm.lemmaK (eq_attns' ~~ map (fn eq => [([eq], [])]) eqs')
-            |> snd
-          end;
-
-    fun after_qed wits eqs = ProofContext.theory (fold_map store_reg (regs ~~ wits)
-      #-> (fn regs => store_eqns_activate regs eqs));
+    fun after_qed witss eqns = ProofContext.theory (note_eqns eqns
+      #-> (fn eqns => fold (fn ((dep, morph), wits) =>
+        Locale.add_registration_eqs (dep, morph $> Element.satisfy_morphism
+          (map (Element.morph_witness export') wits)) eqns export) (deps ~~ witss)));
 
   in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
 
@@ -868,12 +832,33 @@
 end;
 
 
+(** Interpretation between locales: declaring sublocale relationships **)
+
+local
+
+fun gen_sublocale prep_expr intern raw_target expression thy =
+  let
+    val target = intern thy raw_target;
+    val target_ctxt = Locale.init target thy;
+    val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
+    fun after_qed witss = ProofContext.theory
+      (fold (fn ((dep, morph), wits) => Locale.add_dependency
+        target (dep, morph $> Element.satisfy_morphism wits) export) (deps ~~ witss));
+  in Element.witness_proof after_qed propss goal_ctxt end;
+
+in
+
+fun sublocale x = gen_sublocale cert_goal_expression (K I) x;
+fun sublocale_cmd x = gen_sublocale read_goal_expression Locale.intern x;
+
+end;
+
+
 (** Interpretation in proof contexts **)
 
 local
 
-fun gen_interpret prep_expr
-    expression int state =
+fun gen_interpret prep_expr expression int state =
   let
     val _ = Proof.assert_forward_or_chain state;
     val ctxt = Proof.context_of state;

--- a/src/Pure/Isar/locale.ML	Wed Jul 15 10:11:13 2009 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Jul 15 18:20:08 2009 +0200
@@ -70,8 +70,8 @@
   (* Registrations and dependencies *)
   val add_registration: string * (morphism * morphism) -> theory -> theory
   val amend_registration: morphism -> string * morphism -> theory -> theory
-  val add_dependencies: string -> ((string * morphism) * Element.witness list) list ->
-    morphism  -> theory -> theory
+  val add_registration_eqs: string * morphism -> thm list -> morphism -> theory -> theory
+  val add_dependency: string -> string * morphism -> morphism -> theory -> theory
 
   (* Diagnostic *)
   val print_locales: theory -> unit
@@ -368,14 +368,22 @@
       (fn ((name, (base, export)), stamp) => ((name, (base $> morph, export)), stamp))) thy
   end;
 
+fun add_registration_eqs (dep, proto_morph) eqns export thy =
+  let
+    val morph = if null eqns then proto_morph
+      else proto_morph $> Element.eq_morphism thy eqns;
+  in
+    thy
+    |> add_registration (dep, (morph, export))
+    |> Context.theory_map (activate_facts (dep, morph $> export))
+  end;
+
 
 (*** Dependencies ***)
 
-fun add_dependencies loc deps_witss export thy =
+fun add_dependency loc (dep, morph) export thy =
   thy
-  |> fold (fn ((dep, morph), wits) => (change_locale loc o apsnd)
-      (cons ((dep, morph $> Element.satisfy_morphism wits $> export), stamp ())))
-        deps_witss
+  |> (change_locale loc o apsnd) (cons ((dep, morph $> export), stamp ()))
   |> (fn thy => fold_rev (Context.theory_map o activate_facts)
       (all_registrations thy) thy);