--- 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
*)
--- 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
*)
--- 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)
*)
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
*)
--- 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.
--- 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) =