# HG changeset patch
# User ballarin
# Date 1229436577 -3600
# Node ID 51526dd8da8ec0a93ec65bae62ab9327f229b276
# Parent  2d62b637fa8034f804fccd4aa5bbe3d4ab0c195c# Parent  a1c992fb3184e8952f30dbd9e62967eb1d77e6ff
Merged.

diff -r 2d62b637fa80 -r 51526dd8da8e src/FOL/ex/NewLocaleTest.thy
--- a/src/FOL/ex/NewLocaleTest.thy	Tue Dec 16 15:09:12 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy	Tue Dec 16 15:09:37 2008 +0100
@@ -167,6 +167,13 @@
 lemma (in semi_hom_loc) "h(prod(x, y)) = sum(h(x), h(y))"
   by (rule semi_hom_mult)
 
+(* Referring to facts from within a context specification *)
+
+lemma
+  assumes x: "P <-> P"
+  notes y = x
+  shows True ..
+
 
 section {* Theorem statements *}
 
diff -r 2d62b637fa80 -r 51526dd8da8e src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Tue Dec 16 15:09:12 2008 +0100
+++ b/src/Pure/Isar/element.ML	Tue Dec 16 15:09:37 2008 +0100
@@ -23,6 +23,10 @@
   val facts_map: (('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt) ->
    (Attrib.binding * ('fact * Attrib.src list) list) list ->
    (Attrib.binding * ('c * Attrib.src list) list) list
+  val map_ctxt': {binding: Binding.T -> Binding.T,
+    var: Binding.T * mixfix -> Binding.T * mixfix,
+    typ: 'typ -> 'a, term: 'term -> 'b, pat: 'term -> 'b, fact: 'fact -> 'c,
+    attrib: Attrib.src -> Attrib.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
   val map_ctxt: {binding: Binding.T -> Binding.T,
     var: Binding.T * mixfix -> Binding.T * mixfix,
     typ: 'typ -> 'a, term: 'term -> 'b, fact: 'fact -> 'c,
@@ -74,10 +78,8 @@
   val generalize_facts: Proof.context -> Proof.context ->
     (Attrib.binding * (thm list * Attrib.src list) list) list ->
     (Attrib.binding * (thm list * Attrib.src list) list) list
-  val activate: (typ, term, Facts.ref) ctxt list -> Proof.context ->
-    (context_i list * (Binding.T * Thm.thm list) list) * Proof.context
-  val activate_i: context_i list -> Proof.context ->
-    (context_i list * (Binding.T * Thm.thm list) list) * Proof.context
+  val activate: (typ, term, Facts.ref) ctxt list -> Proof.context -> context_i list * Proof.context
+  val activate_i: context_i list -> Proof.context -> context_i list * Proof.context
 end;
 
 structure Element: ELEMENT =
@@ -109,18 +111,22 @@
 
 fun facts_map f facts = Notes ("", facts) |> f |> (fn Notes (_, facts') => facts');
 
-fun map_ctxt {binding, var, typ, term, fact, attrib} =
+fun map_ctxt' {binding, var, typ, term, pat, fact, attrib} =
   fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) =>
        let val (x', mx') = var (x, mx) in (x', Option.map typ T, mx') end))
    | Constrains xs => Constrains (xs |> map (fn (x, T) =>
        let val x' = Binding.base_name (#1 (var (Binding.name x, NoSyn))) in (x', typ T) end))
    | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
-      ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map term ps)))))
+      ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map pat ps)))))
    | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
-      ((binding a, map attrib atts), (term t, map term ps))))
+      ((binding a, map attrib atts), (term t, map pat ps))))
    | Notes (kind, facts) => Notes (kind, facts |> map (fn ((a, atts), bs) =>
       ((binding a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts)))));
 
+fun map_ctxt {binding, var, typ, term, fact, attrib} =
+  map_ctxt' {binding = binding, var = var, typ = typ, term = term, pat = term,
+    fact = fact, attrib = attrib}
+
 fun map_ctxt_attrib attrib =
   map_ctxt {binding = I, var = I, typ = I, term = I, fact = I, attrib = attrib};
 
@@ -536,9 +542,9 @@
 local
 
 fun activate_elem (Fixes fixes) ctxt =
-      ([], ctxt |> ProofContext.add_fixes_i fixes |> snd)
+      ctxt |> ProofContext.add_fixes_i fixes |> snd
   | activate_elem (Constrains _) ctxt =
-      ([], ctxt)
+      ctxt
   | activate_elem (Assumes asms) ctxt =
       let
         val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
@@ -546,7 +552,7 @@
         val (_, ctxt') =
           ctxt |> fold Variable.auto_fixes ts
           |> ProofContext.add_assms_i Assumption.presume_export asms';
-      in ([], ctxt') end
+      in ctxt' end
   | activate_elem (Defines defs) ctxt =
       let
         val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
@@ -556,19 +562,20 @@
         val (_, ctxt') =
           ctxt |> fold (Variable.auto_fixes o #1) asms
           |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
-      in ([], ctxt') end
+      in ctxt' end
   | activate_elem (Notes (kind, facts)) ctxt =
       let
         val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
         val (res, ctxt') = ctxt |> ProofContext.note_thmss_i kind facts';
-      in ((map (#1 o #1) facts' ~~ map #2 res), ctxt') end;
+      in ctxt' end;
 
 fun gen_activate prep_facts raw_elems ctxt =
   let
-    val elems = map (map_ctxt_attrib Args.assignable o prep_facts ctxt) raw_elems;
-    val (res, ctxt') = fold_map activate_elem elems (ProofContext.qualified_names ctxt);
-    val elems' = elems |> map (map_ctxt_attrib Args.closure);
-  in ((elems', flat res), ProofContext.restore_naming ctxt ctxt') end;
+    fun activate elem ctxt =
+      let val elem' = (map_ctxt_attrib Args.assignable o prep_facts ctxt) elem
+      in (elem', activate_elem elem' ctxt) end
+    val (elems, ctxt') = fold_map activate raw_elems (ProofContext.qualified_names ctxt);
+  in (elems |> map (map_ctxt_attrib Args.closure), ProofContext.restore_naming ctxt ctxt') end;
 
 fun check_name name =
   if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name)
diff -r 2d62b637fa80 -r 51526dd8da8e src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Tue Dec 16 15:09:12 2008 +0100
+++ b/src/Pure/Isar/expression.ML	Tue Dec 16 15:09:37 2008 +0100
@@ -184,12 +184,15 @@
 (** Parsing **)
 
 fun parse_elem prep_typ prep_term ctxt elem =
-  Element.map_ctxt {binding = I, var = I, typ = prep_typ ctxt,
-    term = prep_term ctxt, fact = I, attrib = I} elem;
+  Element.map_ctxt' {binding = I, var = I, typ = prep_typ ctxt,
+  term = prep_term (ProofContext.set_mode ProofContext.mode_schematic ctxt), (* FIXME ?? *)
+  pat = prep_term (ProofContext.set_mode ProofContext.mode_pattern ctxt),
+  fact = I, attrib = I} elem;
 
 fun parse_concl prep_term ctxt concl =
   (map o map) (fn (t, ps) =>
-    (prep_term ctxt, map (prep_term ctxt) ps)) concl;
+    (prep_term (ProofContext.set_mode ProofContext.mode_schematic ctxt) t, (* FIXME ?? *)
+      map (prep_term (ProofContext.set_mode ProofContext.mode_pattern ctxt)) ps)) concl;
 
 
 (** Simultaneous type inference: instantiations + elements + conclusion **)
@@ -398,14 +401,12 @@
       let
         val ctxt' = declare_elem prep_vars raw_elem ctxt;
         val elems' = elems @ [parse_elem parse_typ parse_prop ctxt' raw_elem];
-        (* FIXME term bindings *)
         val (_, _, _, ctxt'') = check_autofix insts elems' [] ctxt';
       in (insts, elems', ctxt') end;
 
     fun prep_concl raw_concl (insts, elems, ctxt) =
       let
-        val concl = (map o map) (fn (t, ps) =>
-          (parse_prop ctxt t, map (parse_prop ctxt) ps)) raw_concl;
+        val concl = parse_concl parse_prop ctxt raw_concl;
       in check_autofix insts elems concl ctxt end;
 
     val fors = prep_vars fixed context |> fst;
@@ -485,7 +486,7 @@
     val context' = context |>
       ProofContext.add_fixes_i fixed |> snd |>
       fold NewLocale.activate_local_facts deps;
-    val ((elems', _), _) = activate elems (ProofContext.set_stmt true context');
+    val (elems', _) = activate elems (ProofContext.set_stmt true context');
   in ((fixed, deps, elems'), (parms, spec, defs)) end;
 
 in
diff -r 2d62b637fa80 -r 51526dd8da8e src/Pure/Isar/new_locale.ML
--- a/src/Pure/Isar/new_locale.ML	Tue Dec 16 15:09:12 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML	Tue Dec 16 15:09:37 2008 +0100
@@ -287,18 +287,19 @@
       fold_rev (fn (decl, _) => Context.proof_map (decl morph)) term_decls
   end;
 
-fun activate_notes activ_elem thy (name, morph) input =
+fun activate_notes activ_elem transfer thy (name, morph) input =
   let
     val Loc {notes, ...} = the_locale thy name;
     fun activate ((kind, facts), _) input =
       let
-        val facts' = facts |> Element.facts_map (Element.morph_ctxt morph)
+        val facts' = facts |> Element.facts_map (Element.morph_ctxt
+          (Morphism.thm_morphism (transfer input) $> morph))
       in activ_elem (Notes (kind, facts')) input end;
   in
     fold_rev activate notes input
   end;
 
-fun activate_all name thy activ_elem (marked, input) =
+fun activate_all name thy activ_elem transfer (marked, input) =
   let
     val Loc {parameters = (_, params), spec = (asm, defs), ...} =
       the_locale thy name;
@@ -310,7 +311,7 @@
       (if not (null defs)
         then activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs))
         else I) |>
-      pair marked |> roundup thy (activate_notes activ_elem) (name, Morphism.identity)
+      pair marked |> roundup thy (activate_notes activ_elem transfer) (name, Morphism.identity)
   end;
 
 
@@ -354,15 +355,18 @@
   roundup thy activate_decls dep (get_local_idents ctxt, ctxt) |> uncurry put_local_idents;
 
 fun activate_global_facts dep thy =
-  roundup thy (activate_notes init_global_elem) dep (get_global_idents thy, thy) |>
+  roundup thy (activate_notes init_global_elem transfer) dep (get_global_idents thy, thy) |>
   uncurry put_global_idents;
 
 fun activate_local_facts dep ctxt =
-  roundup (ProofContext.theory_of ctxt) (activate_notes init_local_elem) dep
+  roundup (ProofContext.theory_of ctxt) (activate_notes init_local_elem
+      (transfer o ProofContext.theory_of)) dep
     (get_local_idents ctxt, ctxt) |>
   uncurry put_local_idents;
 
-fun init name thy = activate_all name thy init_local_elem (empty, ProofContext.init thy) |>
+fun init name thy =
+  activate_all name thy init_local_elem (transfer o ProofContext.theory_of)
+    (empty, ProofContext.init thy) |>
   uncurry put_local_idents;
 
 fun print_locale thy show_facts name =
@@ -371,7 +375,7 @@
     val ctxt = init name' thy
   in
     Pretty.big_list "locale elements:"
-      (activate_all name' thy (cons_elem show_facts) (empty, []) |> snd |> rev |> 
+      (activate_all name' thy (cons_elem show_facts) (K I) (empty, []) |> snd |> rev |> 
         map (Element.pretty_ctxt ctxt) |> map Pretty.chunks) |> Pretty.writeln
   end
 
@@ -420,7 +424,7 @@
 
 fun add_thmss loc kind args ctxt =
   let
-    val (([Notes args'], _), ctxt') = Element.activate_i [Notes (kind, args)] ctxt;
+    val ([Notes args'], ctxt') = Element.activate_i [Notes (kind, args)] ctxt;
     val ctxt'' = ctxt' |> ProofContext.theory (
       change_locale loc
         (fn (parameters, spec, decls, notes, dependencies) =>