# HG changeset patch
# User wenzelm
# Date 1027462370 -7200
# Node ID 63462ccc6fac2ee91702444f6b6dd58318db09c3
# Parent  15597d5020356646ff5e1bb11c3a276044bfe052
tuned view;

diff -r 15597d502035 -r 63462ccc6fac src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Jul 24 00:11:56 2002 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Jul 24 00:12:50 2002 +0200
@@ -40,10 +40,10 @@
   val locale_facts_i: theory -> string -> thm list
   val read_context_statement: xstring option -> context attribute element list ->
     (string * (string list * string list)) list list -> context ->
-    string option * cterm option * context * context * (term * (term list * term list)) list list
+    string option * cterm list * context * context * (term * (term list * term list)) list list
   val cert_context_statement: string option -> context attribute element_i list ->
     (term * (term list * term list)) list list -> context ->
-    string option * cterm option * context * context * (term * (term list * term list)) list list
+    string option * cterm list * context * context * (term * (term list * term list)) list list
   val print_locales: theory -> unit
   val print_locale: theory -> expr -> context attribute element list -> unit
   val add_locale: bool -> bstring -> expr -> context attribute element list -> theory -> theory
@@ -89,16 +89,8 @@
 type 'att element = (string, string, string, 'att) elem_expr;
 type 'att element_i = (typ, term, thm list, 'att) elem_expr;
 
-type view = (cterm * thm list) option;
-
-fun view_statement (None: view) = None
-  | view_statement (Some (ct, _)) = Some ct;
-
-fun view_axioms (None: view) = []
-  | view_axioms (Some (_, axs)) = axs;
-
 type locale =
- {view: view,                                             (*external view on assumptions*)
+ {view: cterm list * thm list,                            (*external view on assumptions*)
   import: expr,                                                         (*dynamic import*)
   elems: ((typ, term, thm list, context attribute) elem * stamp) list,  (*static content*)
   params: (string * typ option) list * string list};                  (*all/local params*)
@@ -722,14 +714,14 @@
   let
     val thy = ProofContext.theory_of ctxt;
     val locale = apsome (prep_locale (Theory.sign_of thy)) raw_locale;
-    val (view, fixed_params, import) =
-      (case locale of None => (None, [], empty)
+    val ((view_statement, view_axioms), fixed_params, import) =
+      (case locale of None => (([], []), [], empty)
       | Some name =>
         let val {view, params = (ps, _), ...} = the_locale thy name
         in (view, param_types ps, Locale name) end);
     val ((((locale_ctxt, _), (elems_ctxt, _)), _), concl') =
-      prep_ctxt false (view_axioms view) fixed_params import elems concl ctxt;
-  in (locale, view_statement view, locale_ctxt, elems_ctxt, concl') end;
+      prep_ctxt false view_axioms fixed_params import elems concl ctxt;
+  in (locale, view_statement, locale_ctxt, elems_ctxt, concl') end;
 
 fun gen_facts prep_locale thy name =
   let val ((((_, (_, facts)), _), _), _) = thy |> ProofContext.init
@@ -845,9 +837,9 @@
   let
     val args' = map (fn ((a, ths), atts) => ((a, atts), [(ths, [])])) args;
     val thy' = put_facts loc args' thy;
-    val {view, ...} = the_locale thy loc;
+    val {view = (_, view_axioms), ...} = the_locale thy loc;
     val ((ctxt', _), (_, facts')) =
-      activate_facts (K I) ((ctxt, view_axioms view), [((loc, []), [Notes args'])]);
+      activate_facts (K I) ((ctxt, view_axioms), [((loc, []), [Notes args'])]);
   in ((thy', ctxt'), map #1 facts') end;
 
 end;
@@ -901,7 +893,7 @@
     val defs_sign = Theory.sign_of defs_thy;
     val cert = Thm.cterm_of defs_sign;
 
-    val intro = Tactic.prove_standard defs_sign [] [] statement (fn _ =>
+    val intro = Tactic.prove_standard defs_sign [] ts' statement (fn _ =>
       Tactic.rewrite_goals_tac [pred_def] THEN
       Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
       Tactic.compose_tac (false, Drule.conj_intr_list (map (Thm.assume o cert) ts'), 0) 1);
@@ -947,7 +939,7 @@
           |> #1 |> rpair (elemss', [statement])
         end;
     val (thy'', view) =
-      if Library.null more_ts andalso Library.null ints then (thy', None)
+      if Library.null more_ts andalso Library.null ints then (thy', ([], []))
       else
         let
           val (def_thy, (statement, intro, axioms)) =
@@ -956,7 +948,7 @@
         in
           def_thy |> have_thmss_qualified "" bname
             [((introN, [ContextRules.intro_query_global None]), [([intro], [])])]
-          |> #1 |> rpair (Some (cstatement, axioms))
+          |> #1 |> rpair ([cstatement], axioms)
         end;
   in (thy'', (elemss', view)) end;
 
@@ -979,12 +971,12 @@
       prep_ctxt raw_import raw_body thy_ctxt;
     val elemss = import_elemss @ body_elemss;
 
-    val (pred_thy, (elemss', view)) =
+    val (pred_thy, (elemss', view as (view_statement, view_axioms))) =
       if do_pred then thy |> define_preds bname text elemss
-      else (thy, (elemss, None));
+      else (thy, (elemss, ([], [])));
     val pred_ctxt = ProofContext.init pred_thy;
-    val ((ctxt, _), (_, facts)) = activate_facts (K I) ((pred_ctxt, view_axioms view), elemss')
-    val export = ProofContext.export_standard (view_statement view) ctxt pred_ctxt;
+    val ((ctxt, _), (_, facts)) = activate_facts (K I) ((pred_ctxt, view_axioms), elemss')
+    val export = ProofContext.export_standard view_statement ctxt pred_ctxt;
   in
     pred_thy
     |> have_thmss_qualified "" name (facts |> filter #2 |> map (fn ((a, ths), _) =>
diff -r 15597d502035 -r 63462ccc6fac src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Jul 24 00:11:56 2002 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Jul 24 00:12:50 2002 +0200
@@ -133,16 +133,16 @@
 datatype kind =
   Theorem of {kind: string,
     theory_spec: (bstring * theory attribute list) * theory attribute list list,
-    locale_spec: ((string * (context attribute list * context attribute list list)) *
-      cterm option) option} |
+    locale_spec: (string * (context attribute list * context attribute list list)) option,
+    view: cterm list} |
   Show of context attribute list list |
   Have of context attribute list list;
 
-fun kind_name _ (Theorem {kind = s, theory_spec = ((a, _), _), locale_spec = None}) =
-      s ^ (if a = "" then "" else " " ^ a)
+fun kind_name _ (Theorem {kind = s, theory_spec = ((a, _), _),
+        locale_spec = None, view = _}) = s ^ (if a = "" then "" else " " ^ a)
   | kind_name sg (Theorem {kind = s, theory_spec = ((a, _), _),
-      locale_spec = Some ((name, _), _)}) =
-        s ^ " (in " ^ Locale.cond_extern sg name ^ ")" ^ (if a = "" then "" else " " ^ a)
+        locale_spec = Some (name, _), view = _}) =
+      s ^ " (in " ^ Locale.cond_extern sg name ^ ")" ^ (if a = "" then "" else " " ^ a)
   | kind_name _ (Show _) = "show"
   | kind_name _ (Have _) = "have";
 
@@ -692,8 +692,6 @@
     val init = init_state thy;
     val (opt_name, view, locale_ctxt, elems_ctxt, propp) =
       prep (apsome fst raw_locale) elems (map snd concl) (context_of init);
-    val locale_spec =
-      (case raw_locale of None => None | Some (_, x) => Some ((the opt_name, x), view));
   in
     init
     |> open_block
@@ -701,7 +699,10 @@
     |> open_block
     |> map_context (K elems_ctxt)
     |> setup_goal I ProofContext.bind_propp_schematic_i ProofContext.fix_frees
-      (Theorem {kind = kind, theory_spec = (a, map (snd o fst) concl), locale_spec = locale_spec})
+      (Theorem {kind = kind,
+        theory_spec = (a, map (snd o fst) concl),
+        locale_spec = (case raw_locale of None => None | Some (_, x) => Some (the opt_name, x)),
+        view = view})
       Seq.single true (map (fst o fst) concl) propp
   end;
 
@@ -802,19 +803,18 @@
     val (goal_ctxt, (((kind, names, tss), (_, raw_thm)), _)) = current_goal state;
     val locale_ctxt = context_of (state |> close_block);
     val theory_ctxt = context_of (state |> close_block |> close_block);
-    val {kind = k, theory_spec = ((name, atts), attss), locale_spec} =
+    val {kind = k, theory_spec = ((name, atts), attss), locale_spec, view} =
       (case kind of Theorem x => x | _ => err_malformed "finish_global" state);
-    val view = (case locale_spec of Some (_, Some view) => Some view | _ => None);
 
     val ts = flat tss;
-    val locale_results = map (ProofContext.export_standard None goal_ctxt locale_ctxt)
+    val locale_results = map (ProofContext.export_standard [] goal_ctxt locale_ctxt)
       (prep_result state ts raw_thm);
     val results = map (Drule.strip_shyps_warning o
       ProofContext.export_standard view locale_ctxt theory_ctxt) locale_results;
 
     val (theory', results') =
       theory_of state
-      |> (case locale_spec of None => I | Some ((loc, (loc_atts, loc_attss)), view) => fn thy =>
+      |> (case locale_spec of None => I | Some (loc, (loc_atts, loc_attss)) => fn thy =>
         if length names <> length loc_attss then
           raise THEORY ("Bad number of locale attributes", [thy])
         else (thy, locale_ctxt)
@@ -823,10 +823,10 @@
             if name = "" andalso null loc_atts then thy'
             else (thy', ctxt')
               |> (#1 o #1 o Locale.add_thmss loc [((name, flat (map #2 res)), loc_atts)])))
-      |> Locale.smart_have_thmss k (apsome #1 locale_spec)
+      |> Locale.smart_have_thmss k locale_spec
         ((names ~~ attss) ~~ map (single o Thm.no_attributes) (Library.unflat tss results))
       |> (fn (thy, res) => (thy, res)
-          |>> (#1 o Locale.smart_have_thmss k (apsome #1 locale_spec)
+          |>> (#1 o Locale.smart_have_thmss k locale_spec
             [((name, atts), [(flat (map #2 res), [])])]));
   in (theory', ((k, name), results')) end;
 
diff -r 15597d502035 -r 63462ccc6fac src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Jul 24 00:11:56 2002 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Jul 24 00:12:50 2002 +0200
@@ -48,7 +48,7 @@
   val generalize: context -> context -> term list -> term list
   val find_free: term -> string -> term option
   val export: bool -> context -> context -> thm -> thm Seq.seq
-  val export_standard: cterm option -> context -> context -> thm -> thm
+  val export_standard: cterm list -> context -> context -> thm -> thm
   val drop_schematic: indexname * term option -> indexname * term option
   val add_binds: (indexname * string option) list -> context -> context
   val add_binds_i: (indexname * term option) list -> context -> context
@@ -731,7 +731,7 @@
 
 fun find_free t x = foldl_aterms (get_free x) (None, t);
 
-fun export0 view is_goal inner outer =
+fun export_view view is_goal inner outer =
   let
     val gen = generalize_tfrees inner outer;
     val fixes = fixed_names_of inner \\ fixed_names_of outer;
@@ -740,7 +740,7 @@
   in fn thm => thm
     |> Tactic.norm_hhf_rule
     |> Seq.EVERY (rev exp_asms)
-    |> Seq.map (case view of None => I | Some A => Thm.implies_intr A)
+    |> Seq.map (Drule.implies_intr_list view)
     |> Seq.map (fn rule =>
       let
         val {sign, prop, ...} = Thm.rep_thm rule;
@@ -754,10 +754,10 @@
       end)
   end;
 
-val export = export0 None;
+val export = export_view [];
 
 fun export_standard view inner outer =
-  let val exp = export0 view false inner outer in
+  let val exp = export_view view false inner outer in
     fn th =>
       (case Seq.pull (exp th) of
         Some (th', _) => th' |> Drule.local_standard