# HG changeset patch
# User wenzelm
# Date 1331587367 -3600
# Node ID 38171cab67ae448d0ae73c0c419f0435cf6523a6
# Parent  75208a489363b91d472cd5d0475bb612bd79ed8c# Parent  b81f1de9f57e326cff698286e4752f331eaa6f4c
merged;

diff -r 75208a489363 -r 38171cab67ae src/HOL/Import/HOL4/Template/GenHOL4Base.thy
--- a/src/HOL/Import/HOL4/Template/GenHOL4Base.thy	Mon Mar 12 22:11:10 2012 +0100
+++ b/src/HOL/Import/HOL4/Template/GenHOL4Base.thy	Mon Mar 12 22:22:47 2012 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Import/Generate-HOL/GenHOL4Base.thy
+(*  Title:      HOL/Import/HOL4/Template/GenHOL4Base.thy
     Author:     Sebastian Skalberg, TU Muenchen
 *)
 
diff -r 75208a489363 -r 38171cab67ae src/HOL/Import/HOL4/Template/GenHOL4Prob.thy
--- a/src/HOL/Import/HOL4/Template/GenHOL4Prob.thy	Mon Mar 12 22:11:10 2012 +0100
+++ b/src/HOL/Import/HOL4/Template/GenHOL4Prob.thy	Mon Mar 12 22:22:47 2012 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Import/Generate-HOL/GenHOL4Prob.thy
+(*  Title:      HOL/Import/HOL4/Template/GenHOL4Prob.thy
     Author:     Sebastian Skalberg, TU Muenchen
 *)
 
diff -r 75208a489363 -r 38171cab67ae src/HOL/Import/HOL4/Template/GenHOL4Real.thy
--- a/src/HOL/Import/HOL4/Template/GenHOL4Real.thy	Mon Mar 12 22:11:10 2012 +0100
+++ b/src/HOL/Import/HOL4/Template/GenHOL4Real.thy	Mon Mar 12 22:22:47 2012 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Import/Generate-HOL/GenHOL4Real.thy
+(*  Title:      HOL/Import/HOL4/Template/GenHOL4Real.thy
     Author:     Sebastian Skalberg (TU Muenchen)
 *)
 
diff -r 75208a489363 -r 38171cab67ae src/HOL/Import/HOL4/Template/GenHOL4Vec.thy
--- a/src/HOL/Import/HOL4/Template/GenHOL4Vec.thy	Mon Mar 12 22:11:10 2012 +0100
+++ b/src/HOL/Import/HOL4/Template/GenHOL4Vec.thy	Mon Mar 12 22:22:47 2012 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Import/Generate-HOL/GenHOL4Vec.thy
+(*  Title:      HOL/Import/HOL4/Template/GenHOL4Vec.thy
     Author:     Sebastian Skalberg, TU Muenchen
 *)
 
diff -r 75208a489363 -r 38171cab67ae src/HOL/Import/HOL4/Template/GenHOL4Word32.thy
--- a/src/HOL/Import/HOL4/Template/GenHOL4Word32.thy	Mon Mar 12 22:11:10 2012 +0100
+++ b/src/HOL/Import/HOL4/Template/GenHOL4Word32.thy	Mon Mar 12 22:22:47 2012 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Import/Generate-HOL/GenHOL4Word32.thy
+(*  Title:      HOL/Import/HOL4/Template/GenHOL4Word32.thy
     Author:     Sebastian Skalberg, TU Muenchen
 *)
 
diff -r 75208a489363 -r 38171cab67ae src/HOL/Import/HOL_Light/HOLLightInt.thy
--- a/src/HOL/Import/HOL_Light/HOLLightInt.thy	Mon Mar 12 22:11:10 2012 +0100
+++ b/src/HOL/Import/HOL_Light/HOLLightInt.thy	Mon Mar 12 22:22:47 2012 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Import/HOLLightInt.thy
+(*  Title:      HOL/Import/HOL_Light/HOLLightInt.thy
     Author:     Cezary Kaliszyk
 *)
 
diff -r 75208a489363 -r 38171cab67ae src/HOL/Import/HOL_Light/HOLLightList.thy
--- a/src/HOL/Import/HOL_Light/HOLLightList.thy	Mon Mar 12 22:11:10 2012 +0100
+++ b/src/HOL/Import/HOL_Light/HOLLightList.thy	Mon Mar 12 22:22:47 2012 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Import/HOLLightList.thy
+(*  Title:      HOL/Import/HOL_Light/HOLLightList.thy
     Author:     Cezary Kaliszyk
 *)
 
diff -r 75208a489363 -r 38171cab67ae src/HOL/Import/HOL_Light/HOLLightReal.thy
--- a/src/HOL/Import/HOL_Light/HOLLightReal.thy	Mon Mar 12 22:11:10 2012 +0100
+++ b/src/HOL/Import/HOL_Light/HOLLightReal.thy	Mon Mar 12 22:22:47 2012 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Import/HOLLightReal.thy
+(*  Title:      HOL/Import/HOL_Light/HOLLightReal.thy
     Author:     Cezary Kaliszyk
 *)
 
diff -r 75208a489363 -r 38171cab67ae src/HOL/Import/HOL_Light/Template/GenHOLLight.thy
--- a/src/HOL/Import/HOL_Light/Template/GenHOLLight.thy	Mon Mar 12 22:11:10 2012 +0100
+++ b/src/HOL/Import/HOL_Light/Template/GenHOLLight.thy	Mon Mar 12 22:22:47 2012 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Import/Generate-HOLLight/GenHOLLight.thy
+(*  Title:      HOL/Import/HOL_Light/Template/GenHOLLight.thy
     Author:     Steven Obua, TU Muenchen
     Author:     Cezary Kaliszyk
 *)
diff -r 75208a489363 -r 38171cab67ae src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Mon Mar 12 22:11:10 2012 +0100
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Mon Mar 12 22:22:47 2012 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/ex/Quickcheck_Examples.thy
+(*  Title:      HOL/Quickcheck_Examples/Quickcheck_Examples.thy
     Author:     Stefan Berghofer, Lukas Bulwahn
     Copyright   2004 - 2010 TU Muenchen
 *)
diff -r 75208a489363 -r 38171cab67ae src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy	Mon Mar 12 22:11:10 2012 +0100
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy	Mon Mar 12 22:22:47 2012 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/ex/Quickcheck_Lattice_Examples.thy
+(*  Title:      HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy
     Author:     Lukas Bulwahn
     Copyright   2010 TU Muenchen
 *)
diff -r 75208a489363 -r 38171cab67ae src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy	Mon Mar 12 22:11:10 2012 +0100
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy	Mon Mar 12 22:22:47 2012 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/ex/Quickcheck_Narrowing_Examples.thy
+(*  Title:      HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy
     Author:     Lukas Bulwahn
     Copyright   2011 TU Muenchen
 *)
diff -r 75208a489363 -r 38171cab67ae src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Mon Mar 12 22:11:10 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Mon Mar 12 22:22:47 2012 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/TPTP/?/tptp_interpret.ML
+(*  Title:      HOL/TPTP/TPTP_Parser/tptp_interpret.ML
     Author:     Nik Sultana, Cambridge University Computer Laboratory
 
 Interprets TPTP problems in Isabelle/HOL.
diff -r 75208a489363 -r 38171cab67ae src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Mar 12 22:11:10 2012 +0100
+++ b/src/Pure/Isar/locale.ML	Mon Mar 12 22:22:47 2012 +0100
@@ -72,6 +72,7 @@
   val amend_registration: string * morphism -> morphism * bool ->
     morphism -> Context.generic -> Context.generic
   val registrations_of: Context.generic -> string -> (string * morphism) list
+  val all_registrations_of: Context.generic -> (string * morphism) list
   val add_dependency: string -> string * morphism -> (morphism * bool) option ->
     morphism -> theory -> theory
 
@@ -205,12 +206,10 @@
 fun mixins_of thy name serial = the_locale thy name |>
   #mixins |> lookup_mixins serial;
 
-(* unused *)
+(* FIXME unused *)
 fun identity_on thy name morph =
   let val mk_instance = instance_of thy name
-  in
-    forall2 (curry Term.aconv_untyped) (mk_instance Morphism.identity) (mk_instance morph)
-  end;
+  in ListPair.all Term.aconv_untyped (mk_instance Morphism.identity, mk_instance morph) end;
 
 (* Print instance and qualifiers *)
 
@@ -382,7 +381,7 @@
 fun registrations_of context name =
   get_registrations context (filter (curry (op =) name o fst o fst));
 
-fun all_registrations context = get_registrations context I;
+fun all_registrations_of context = get_registrations context I;
 
 
 (*** Activate context elements of locale ***)
@@ -401,17 +400,16 @@
 fun activate_notes activ_elem transfer context export' (name, morph) input =
   let
     val thy = Context.theory_of context;
-    val {notes, ...} = the_locale thy name;
-    fun activate ((kind, facts), _) input =
-      let
-        val mixin =
-          (case export' of
-            NONE => Morphism.identity
-          | SOME export => collect_mixins context (name, morph $> export) $> export);
-        val facts' = facts |> Element.transform_facts (transfer input $> morph $> mixin);
-      in activ_elem (Notes (kind, facts')) input end;
+    val mixin =
+      (case export' of
+        NONE => Morphism.identity
+      | SOME export => collect_mixins context (name, morph $> export) $> export);
+    val morph' = transfer input $> morph $> mixin;
+    val notes' =
+      Par_List.map (Element.transform_ctxt morph' o Notes o #1) (#notes (the_locale thy name));
   in
-    fold_rev activate notes input
+    fold_rev (fn elem => fn res => activ_elem (Element.transform_ctxt (transfer res) elem) res)
+      notes' input
   end;
 
 fun activate_all name thy activ_elem transfer (marked, input) =