# HG changeset patch
# User ballarin
# Date 1071148227 -3600
# Node ID 61df18481f5361231d77755cabe4ec3dd9514df6
# Parent  84fda1b3994719ca4e3f1caaa3e87f941f823861
Change to prune_prems in Pure/Isar/locale.ML.

diff -r 84fda1b39947 -r 61df18481f53 src/HOL/Real/HahnBanach/HahnBanach.thy
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Thu Dec 11 10:52:41 2003 +0100
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Thu Dec 11 14:10:27 2003 +0100
@@ -340,7 +340,7 @@
   have F: "vectorspace F" ..
   have linearform: "linearform F f" .
   have F_norm: "normed_vectorspace F norm"
-    by (rule subspace_normed_vs [OF _ _ _ norm.intro])
+    by (rule subspace_normed_vs [OF _ _ norm.intro])
   have ge_zero: "0 \<le> \<parallel>f\<parallel>\<hyphen>F"
     by (rule normed_vectorspace.fn_norm_ge_zero
       [OF F_norm _ continuous.intro, folded B_def fn_norm_def])
diff -r 84fda1b39947 -r 61df18481f53 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Dec 11 10:52:41 2003 +0100
+++ b/src/Pure/Isar/locale.ML	Thu Dec 11 14:10:27 2003 +0100
@@ -89,7 +89,15 @@
 type 'att element_i = (typ, term, thm list, 'att) elem_expr;
 
 type locale =
- {view: cterm list * thm list,                            (*external view on assumptions*)
+ {view: cterm list * thm list,
+    (* If locale <loc> contains assumptions these are encoded in the
+       predicate <loc>.  If these assumptions are accumulated
+       fragments via import, the context generated when entering the
+       locale will contain a list of assumptions corresponding to the
+       assumptions of all locale fragments.
+       The first part of view (called statement) represents these assumptions,
+       the second part (called axioms) contains projections from <loc> to the
+       assumption fragments. *)
   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*)
@@ -203,17 +211,26 @@
 
 in 
 
-(* Prune premises: remove internal delta predicates.
+(** Prune premises:
+   Remove internal delta predicates (generated by "includes") from the
+   premises of a theorem.
 
    Assumes no outer quanfifiers and no flex-flex pairs.
    May change names of TVars.
-   Performs compress and close_derivation on result, if modified. *)
+   Performs compress and close_derivation on result, if modified. **)
+
+(* Note: reconstruction of the correct premises fails for subspace_normed_vs
+   in HOL/Real/HahnBanach/NormedSpace.thy.  This cannot be fixed since in the
+   current setup there is no way of distinguishing whether the theorem
+   statement involved "includes subspace F E + normed_vectorspace E" or
+   "includes subspace F E + vectorspace E + norm E norm".
+*)
 
 fun prune_prems thy thm = let
   val sign = Theory.sign_of thy;
   fun analyse cprem =
     (* Returns None if head of premise is not a predicate defined by a locale,
-       returns also None if locale has import but predicate is not *_axioms
+       returns also None if locale has a view but predicate is not *_axioms
        since this is a premise that wasn't generated by includes.  *)
     case Term.strip_comb (ObjectLogic.drop_judgment sign (term_of cprem)) of
 	(Const (raw_name, T), args) => let
@@ -221,8 +238,8 @@
               handle LIST _ => raw_name
           in case get_locale thy name of
 		None => None
-	      | Some {import, ...} =>
-                  if name = raw_name andalso import <> empty
+	      | Some {view = (_, axioms), ...} =>
+                  if name = raw_name andalso not (null axioms)
                   then None
                   else Some (((name, args), T), name = raw_name)
           end
@@ -246,7 +263,7 @@
 			     | (trie, Some id) => insert_ident subs id trie)
 			   (Trie [], ids);
     (* Assemble new theorem; new prems will be hyps.
-       Axioms is an intermeditate list of locale axioms required to
+       Axioms is an intermediate list of locale axioms required to
        replace old premises by new ones. *)
     fun scan ((roots, thm, cprems', axioms), (cprem, id)) =
 	  case id of