# HG changeset patch
# User haftmann
# Date 1236757557 -3600
# Node ID aad3cd70e25a2f5f298ad004c6425da76735271e
# Parent  699afca335277d9b7cf3eff68e71e13c20c81db2# Parent  836b71e950b52c7be9b62c0ae47872d00c53633e
merged

diff -r 836b71e950b5 -r aad3cd70e25a Admin/Mercurial/cvsids
--- a/Admin/Mercurial/cvsids	Wed Mar 11 08:45:47 2009 +0100
+++ b/Admin/Mercurial/cvsids	Wed Mar 11 08:45:57 2009 +0100
@@ -1,5 +1,6 @@
 Identifiers of some old CVS file versions
 =========================================
 
-src/Pure/type.ML    1.65        0d984ee030a1
+src/Pure/type.ML            1.65    0d984ee030a1
+src/Pure/General/file.ML    1.18    6cdd6a8da9b9
 
diff -r 836b71e950b5 -r aad3cd70e25a src/HOL/Docs/Main_Doc.thy
--- a/src/HOL/Docs/Main_Doc.thy	Wed Mar 11 08:45:47 2009 +0100
+++ b/src/HOL/Docs/Main_Doc.thy	Wed Mar 11 08:45:57 2009 +0100
@@ -18,16 +18,16 @@
 text{*
 
 \begin{abstract}
-This document lists the main types, functions and syntax provided by theory @{theory Main}. It is meant as a quick overview of what is available. The sophisicated class structure is only hinted at.
+This document lists the main types, functions and syntax provided by theory @{theory Main}. It is meant as a quick overview of what is available. The sophisticated class structure is only hinted at.
 \end{abstract}
 
 \section{HOL}
 
-The basic logic: @{prop "x = y"}, @{const True}, @{const False}, @{prop"Not P"}, @{prop"P & Q"}, @{prop "P | Q"}, @{prop "P --> Q"}, @{prop"ALL x. P"}, @{prop"EX x. P"}, @{prop"EX! x. P"}, @{term"THE x. P"}.
+The basic logic: @{prop "x = y"}, @{const True}, @{const False}, @{prop"Not P"}, @{prop"P & Q"}, @{prop "P | Q"}, @{prop "P --> Q"}, @{prop"ALL x. P"}, @{prop"EX x. P"}, @{prop"EX! x. P"}, @{term"THE x. P"}. (\textsc{ascii}: \verb$~$, \verb$&$, \verb$|$, \verb$-->$, \texttt{ALL}, \texttt{EX})
 
 Overloaded operators:
 
-\begin{supertabular}{@ {} l @ {~::~} l @ {}}
+\begin{supertabular}{@ {} l @ {~::~} l l @ {}}
 @{text "0"} & @{typeof HOL.zero}\\
 @{text "1"} & @{typeof HOL.one}\\
 @{const HOL.plus} & @{typeof HOL.plus}\\
@@ -38,7 +38,7 @@
 @{const HOL.divide} & @{typeof HOL.divide}\\
 @{const HOL.abs} & @{typeof HOL.abs}\\
 @{const HOL.sgn} & @{typeof HOL.sgn}\\
-@{const HOL.less_eq} & @{typeof HOL.less_eq}\\
+@{const HOL.less_eq} & @{typeof HOL.less_eq} & (\verb$<=$)\\
 @{const HOL.less} & @{typeof HOL.less}\\
 @{const HOL.default} & @{typeof HOL.default}\\
 @{const HOL.undefined} & @{typeof HOL.undefined}\\
@@ -109,13 +109,13 @@
 Sets are predicates: @{text[source]"'a set  =  'a \<Rightarrow> bool"}
 \bigskip
 
-\begin{supertabular}{@ {} l @ {~::~} l @ {}}
+\begin{supertabular}{@ {} l @ {~::~} l l @ {}}
 @{const Set.empty} & @{term_type_only "Set.empty" "'a set"}\\
 @{const insert} & @{term_type_only insert "'a\<Rightarrow>'a set\<Rightarrow>'a set"}\\
 @{const Collect} & @{term_type_only Collect "('a\<Rightarrow>bool)\<Rightarrow>'a set"}\\
-@{const "op :"} & @{term_type_only "op :" "'a\<Rightarrow>'a set\<Rightarrow>bool"} \qquad(\textsc{ascii} @{text":"})\\
-@{const Set.Un} & @{term_type_only Set.Un "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} \qquad(\textsc{ascii} @{text"Un"})\\
-@{const Set.Int} & @{term_type_only Set.Int "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} \qquad(\textsc{ascii} @{text"Int"})\\
+@{const "op :"} & @{term_type_only "op :" "'a\<Rightarrow>'a set\<Rightarrow>bool"} & (\texttt{:})\\
+@{const Set.Un} & @{term_type_only Set.Un "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\texttt{Un})\\
+@{const Set.Int} & @{term_type_only Set.Int "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\texttt{Int})\\
 @{const UNION} & @{term_type_only UNION "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\
 @{const INTER} & @{term_type_only INTER "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\
 @{const Union} & @{term_type_only Union "'a set set\<Rightarrow>'a set"}\\
@@ -129,7 +129,7 @@
 
 \subsubsection*{Syntax}
 
-\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
+\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
 @{text"{x\<^isub>1,\<dots>,x\<^isub>n}"} & @{text"insert x\<^isub>1 (\<dots> (insert x\<^isub>n {})\<dots>)"}\\
 @{term"x ~: A"} & @{term[source]"\<not>(x \<in> A)"}\\
 @{term"A \<subseteq> B"} & @{term[source]"A \<le> B"}\\
@@ -137,9 +137,9 @@
 @{term[source]"A \<supseteq> B"} & @{term[source]"B \<le> A"}\\
 @{term[source]"A \<supset> B"} & @{term[source]"B < A"}\\
 @{term"{x. P}"} & @{term[source]"Collect(\<lambda>x. P)"}\\
-@{term[mode=xsymbols]"UN x:I. A"} & @{term[source]"UNION I (\<lambda>x. A)"}\\
+@{term[mode=xsymbols]"UN x:I. A"} & @{term[source]"UNION I (\<lambda>x. A)"} & (\texttt{UN})\\
 @{term[mode=xsymbols]"UN x. A"} & @{term[source]"UNION UNIV (\<lambda>x. A)"}\\
-@{term[mode=xsymbols]"INT x:I. A"} & @{term[source]"INTER I (\<lambda>x. A)"}\\
+@{term[mode=xsymbols]"INT x:I. A"} & @{term[source]"INTER I (\<lambda>x. A)"} & (\texttt{INT})\\
 @{term[mode=xsymbols]"INT x. A"} & @{term[source]"INTER UNIV (\<lambda>x. A)"}\\
 @{term"ALL x:A. P"} & @{term[source]"Ball A (\<lambda>x. P)"}\\
 @{term"EX x:A. P"} & @{term[source]"Bex A (\<lambda>x. P)"}\\
diff -r 836b71e950b5 -r aad3cd70e25a src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Wed Mar 11 08:45:47 2009 +0100
+++ b/src/Pure/General/name_space.ML	Wed Mar 11 08:45:57 2009 +0100
@@ -33,6 +33,8 @@
   val full_name: naming -> binding -> string
   val external_names: naming -> string -> string list
   val add_path: string -> naming -> naming
+  val root_path: naming -> naming
+  val parent_path: naming -> naming
   val no_base_names: naming -> naming
   val qualified_names: naming -> naming
   val sticky_prefix: string -> naming -> naming
@@ -189,10 +191,13 @@
 val default_naming = make_naming ([], false, false);
 
 fun add_path elems = map_naming (fn (path, no_base_names, qualified_names) =>
-  if elems = "//" then ([], no_base_names, true)
-  else if elems = "/" then ([], no_base_names, qualified_names)
-  else if elems = ".." then (perhaps (try (#1 o split_last)) path, no_base_names, qualified_names)
-  else (path @ map (rpair false) (Long_Name.explode elems), no_base_names, qualified_names));
+  (path @ map (rpair false) (Long_Name.explode elems), no_base_names, qualified_names));
+
+val root_path = map_naming (fn (_, no_base_names, qualified_names) =>
+  ([], no_base_names, qualified_names));
+
+val parent_path = map_naming (fn (path, no_base_names, qualified_names) =>
+  (perhaps (try (#1 o split_last)) path, no_base_names, qualified_names));
 
 fun sticky_prefix elems = map_naming (fn (path, no_base_names, qualified_names) =>
   (path @ map (rpair true) (Long_Name.explode elems), no_base_names, qualified_names));
diff -r 836b71e950b5 -r aad3cd70e25a src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Mar 11 08:45:47 2009 +0100
+++ b/src/Pure/Isar/proof.ML	Wed Mar 11 08:45:57 2009 +0100
@@ -677,18 +677,19 @@
 
 local
 
+fun qualified_binding a =
+  Binding.qualify true (Long_Name.qualifier a) (Binding.name (Long_Name.base_name a));
+
 fun gen_invoke_case prep_att (name, xs, raw_atts) state =
   let
     val atts = map (prep_att (theory_of state)) raw_atts;
     val (asms, state') = state |> map_context_result (fn ctxt =>
       ctxt |> ProofContext.apply_case (ProofContext.get_case ctxt name xs));
-    val assumptions = asms |> map (fn (a, ts) => ((Binding.name a, atts), map (rpair []) ts));
+    val assumptions = asms |> map (fn (a, ts) => ((qualified_binding a, atts), map (rpair []) ts));
   in
     state'
-    |> map_context (ProofContext.qualified_names #> ProofContext.no_base_names)
     |> assume_i assumptions
     |> add_binds_i AutoBind.no_facts
-    |> map_context (ProofContext.restore_naming (context_of state))
     |> `the_facts |-> (fn thms => note_thmss_i [((Binding.name name, []), [(thms, [])])])
   end;
 
diff -r 836b71e950b5 -r aad3cd70e25a src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Mar 11 08:45:47 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Wed Mar 11 08:45:57 2009 +0100
@@ -97,9 +97,8 @@
   val get_thms: Proof.context -> xstring -> thm list
   val get_thm: Proof.context -> xstring -> thm
   val add_path: string -> Proof.context -> Proof.context
-  val no_base_names: Proof.context -> Proof.context
+  val sticky_prefix: string -> Proof.context -> Proof.context
   val qualified_names: Proof.context -> Proof.context
-  val sticky_prefix: string -> Proof.context -> Proof.context
   val restore_naming: Proof.context -> Proof.context -> Proof.context
   val reset_naming: Proof.context -> Proof.context
   val note_thmss: string -> (Thm.binding * (Facts.ref * attribute list) list) list ->
@@ -263,9 +262,11 @@
 
 fun transfer_syntax thy =
   map_syntax (LocalSyntax.rebuild thy) #>
-  map_consts (fn (local_consts, _) =>
-    let val thy_consts = Sign.consts_of thy
-    in (Consts.merge (local_consts, thy_consts), thy_consts) end);
+  map_consts (fn consts as (local_consts, global_consts) =>
+    let val thy_consts = Sign.consts_of thy in
+      if Consts.eq_consts (thy_consts, global_consts) then consts
+      else (Consts.merge (local_consts, thy_consts), thy_consts)
+    end);
 
 fun transfer thy = Context.transfer_proof thy #> transfer_syntax thy;
 
@@ -945,9 +946,8 @@
 (* name space operations *)
 
 val add_path        = map_naming o NameSpace.add_path;
-val no_base_names   = map_naming NameSpace.no_base_names;
+val sticky_prefix   = map_naming o NameSpace.sticky_prefix;
 val qualified_names = map_naming NameSpace.qualified_names;
-val sticky_prefix   = map_naming o NameSpace.sticky_prefix;
 val restore_naming  = map_naming o K o naming_of;
 val reset_naming    = map_naming (K local_naming);
 
diff -r 836b71e950b5 -r aad3cd70e25a src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Mar 11 08:45:47 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML	Wed Mar 11 08:45:57 2009 +0100
@@ -293,7 +293,10 @@
 local
 
 fun debugging f x =
-  if ! debug then exception_trace (fn () => f x)
+  if ! debug then
+    (case exception_trace (fn () => SOME (f x) handle UNDEF => NONE) of
+      SOME y => y
+    | NONE => raise UNDEF)
   else f x;
 
 fun toplevel_error f x =
diff -r 836b71e950b5 -r aad3cd70e25a src/Pure/consts.ML
--- a/src/Pure/consts.ML	Wed Mar 11 08:45:47 2009 +0100
+++ b/src/Pure/consts.ML	Wed Mar 11 08:45:57 2009 +0100
@@ -8,6 +8,7 @@
 signature CONSTS =
 sig
   type T
+  val eq_consts: T * T -> bool
   val abbrevs_of: T -> string list -> (term * term) list
   val dest: T ->
    {constants: (typ * term option) NameSpace.table,
@@ -53,6 +54,13 @@
   constraints: typ Symtab.table,
   rev_abbrevs: (term * term) list Symtab.table};
 
+fun eq_consts
+   (Consts {decls = decls1, constraints = constraints1, rev_abbrevs = rev_abbrevs1},
+    Consts {decls = decls2, constraints = constraints2, rev_abbrevs = rev_abbrevs2}) =
+  pointer_eq (decls1, decls2) andalso
+  pointer_eq (constraints1, constraints2) andalso
+  pointer_eq (rev_abbrevs1, rev_abbrevs2);
+
 fun make_consts (decls, constraints, rev_abbrevs) =
   Consts {decls = decls, constraints = constraints, rev_abbrevs = rev_abbrevs};
 
diff -r 836b71e950b5 -r aad3cd70e25a src/Pure/sign.ML
--- a/src/Pure/sign.ML	Wed Mar 11 08:45:47 2009 +0100
+++ b/src/Pure/sign.ML	Wed Mar 11 08:45:57 2009 +0100
@@ -122,13 +122,13 @@
   val add_trrules_i: ast Syntax.trrule list -> theory -> theory
   val del_trrules_i: ast Syntax.trrule list -> theory -> theory
   val add_path: string -> theory -> theory
+  val root_path: theory -> theory
   val parent_path: theory -> theory
-  val root_path: theory -> theory
+  val sticky_prefix: string -> theory -> theory
+  val no_base_names: theory -> theory
+  val qualified_names: theory -> theory
   val absolute_path: theory -> theory
   val local_path: theory -> theory
-  val no_base_names: theory -> theory
-  val qualified_names: theory -> theory
-  val sticky_prefix: string -> theory -> theory
   val restore_naming: theory -> theory -> theory
   val hide_class: bool -> string -> theory -> theory
   val hide_type: bool -> string -> theory -> theory
@@ -619,17 +619,18 @@
 (* naming *)
 
 val add_path        = map_naming o NameSpace.add_path;
+val root_path       = map_naming NameSpace.root_path;
+val parent_path     = map_naming NameSpace.parent_path;
+val sticky_prefix   = map_naming o NameSpace.sticky_prefix;
 val no_base_names   = map_naming NameSpace.no_base_names;
 val qualified_names = map_naming NameSpace.qualified_names;
-val sticky_prefix   = map_naming o NameSpace.sticky_prefix;
-val restore_naming  = map_naming o K o naming_of;
 
-val parent_path   = add_path "..";
-val root_path     = add_path "/";
-val absolute_path = add_path "//";
+val absolute_path = root_path o qualified_names;
 
 fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
 
+val restore_naming  = map_naming o K o naming_of;
+
 
 (* hide names *)