# HG changeset patch
# User wenzelm
# Date 1256748353 -3600
# Node ID 810c161552330d50547d82a7078e582f6a4bd38a
# Parent  9290fbf0a30e9a33afacd48535bf76bbbd0e7e2d# Parent  c6364889fea526dcd1dcb26e746064818c8e495c
merged

diff -r 9290fbf0a30e -r 810c16155233 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Wed Oct 28 12:21:38 2009 +0000
+++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Oct 28 17:45:53 2009 +0100
@@ -567,13 +567,16 @@
     val rep_set_names'' = map (Sign.full_bname thy3) rep_set_names';
 
     val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
-        Inductive.add_inductive_global (serial ())
+      thy3
+      |> Sign.map_naming Name_Space.conceal
+      |> Inductive.add_inductive_global (serial ())
           {quiet_mode = false, verbose = false, kind = Thm.internalK,
            alt_name = Binding.name big_rep_name, coind = false, no_elim = true, no_ind = false,
            skip_mono = true, fork_mono = false}
           (map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
              (rep_set_names' ~~ recTs'))
-          [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] thy3;
+          [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) []
+      ||> Sign.restore_naming thy3;
 
     (**** Prove that representing set is closed under permutation ****)
 
@@ -1508,15 +1511,17 @@
           ([], [], [], [], 0);
 
     val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) =
-      thy10 |>
-        Inductive.add_inductive_global (serial ())
+      thy10
+      |> Sign.map_naming Name_Space.conceal
+      |> Inductive.add_inductive_global (serial ())
           {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
            alt_name = Binding.name big_rec_name, coind = false, no_elim = false, no_ind = false,
            skip_mono = true, fork_mono = false}
           (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
           (map dest_Free rec_fns)
-          (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] ||>
-      PureThy.hide_fact true (Long_Name.append (Sign.full_bname thy10 big_rec_name) "induct");
+          (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []
+      ||> PureThy.hide_fact true (Long_Name.append (Sign.full_bname thy10 big_rec_name) "induct")
+      ||> Sign.restore_naming thy10;
 
     (** equivariance **)
 
diff -r 9290fbf0a30e -r 810c16155233 src/HOL/Tools/Datatype/datatype_abs_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Wed Oct 28 12:21:38 2009 +0000
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Wed Oct 28 17:45:53 2009 +0100
@@ -153,13 +153,17 @@
         (descr' ~~ recTs ~~ rec_sets') ([], 0);
 
     val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
-        Inductive.add_inductive_global (serial ())
+      thy0
+      |> Sign.map_naming Name_Space.conceal
+      |> Inductive.add_inductive_global (serial ())
           {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
             alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true,
             skip_mono = true, fork_mono = false}
           (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
           (map dest_Free rec_fns)
-          (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] thy0;
+          (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []
+      ||> Sign.restore_naming thy0
+      ||> Theory.checkpoint;
 
     (* prove uniqueness and termination of primrec combinators *)
 
diff -r 9290fbf0a30e -r 810c16155233 src/HOL/Tools/Datatype/datatype_rep_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Wed Oct 28 12:21:38 2009 +0000
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Wed Oct 28 17:45:53 2009 +0100
@@ -170,12 +170,16 @@
         ((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names');
 
     val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
-        Inductive.add_inductive_global (serial ())
+      thy1
+      |> Sign.map_naming Name_Space.conceal
+      |> Inductive.add_inductive_global (serial ())
           {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
            alt_name = Binding.name big_rec_name, coind = false, no_elim = true, no_ind = false,
            skip_mono = true, fork_mono = false}
           (map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') []
-          (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] thy1;
+          (map (fn x => (Attrib.empty_binding, x)) intr_ts) []
+      ||> Sign.restore_naming thy1
+      ||> Theory.checkpoint;
 
     (********************************* typedef ********************************)
 
diff -r 9290fbf0a30e -r 810c16155233 src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Wed Oct 28 12:21:38 2009 +0000
+++ b/src/HOL/Tools/Function/function_core.ML	Wed Oct 28 17:45:53 2009 +0100
@@ -488,7 +488,9 @@
               |> Syntax.check_term lthy
 
       val ((f, (_, f_defthm)), lthy) =
-        LocalTheory.define Thm.internalK ((Binding.name (function_name fname), mixfix), ((Binding.name fdefname, []), f_def)) lthy
+        LocalTheory.define Thm.internalK
+          ((Binding.name (function_name fname), mixfix),
+            ((Binding.conceal (Binding.name fdefname), []), f_def)) lthy
     in
       ((f, f_defthm), lthy)
     end
diff -r 9290fbf0a30e -r 810c16155233 src/HOL/Tools/Function/inductive_wrap.ML
--- a/src/HOL/Tools/Function/inductive_wrap.ML	Wed Oct 28 12:21:38 2009 +0000
+++ b/src/HOL/Tools/Function/inductive_wrap.ML	Wed Oct 28 17:45:53 2009 +0100
@@ -39,7 +39,9 @@
 fun inductive_def defs (((R, T), mixfix), lthy) =
     let
       val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) =
-          Inductive.add_inductive_i
+        lthy
+        |> LocalTheory.conceal
+        |> Inductive.add_inductive_i
             {quiet_mode = false,
               verbose = ! Toplevel.debug,
               kind = Thm.internalK,
@@ -53,7 +55,7 @@
             [] (* no parameters *)
             (map (fn t => (Attrib.empty_binding, t)) defs) (* the intros *)
             [] (* no special monos *)
-            lthy
+        ||> LocalTheory.restore_naming lthy
 
       val intrs = map2 (requantify lthy (R, T)) defs intrs_gen
                   
diff -r 9290fbf0a30e -r 810c16155233 src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Wed Oct 28 12:21:38 2009 +0000
+++ b/src/HOL/Tools/Function/mutual.ML	Wed Oct 28 17:45:53 2009 +0100
@@ -146,9 +146,9 @@
       fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy =
           let
             val ((f, (_, f_defthm)), lthy') =
-              LocalTheory.define Thm.internalK ((Binding.name fname, mixfix),
-                                            ((Binding.name (fname ^ "_def"), []), Term.subst_bound (fsum, f_def)))
-                              lthy
+              LocalTheory.define Thm.internalK
+                ((Binding.name fname, mixfix),
+                  (apfst Binding.conceal Attrib.empty_binding, Term.subst_bound (fsum, f_def))) lthy
           in
             (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def,
                          f=SOME f, f_defthm=SOME f_defthm },
diff -r 9290fbf0a30e -r 810c16155233 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed Oct 28 12:21:38 2009 +0000
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed Oct 28 17:45:53 2009 +0100
@@ -368,14 +368,18 @@
         if is_some (try (map (cterm_of thy)) intr_ts) then
           let
             val (ind_result, thy') =
-              Inductive.add_inductive_global (serial ())
+              thy
+              |> Sign.map_naming Name_Space.conceal
+              |> Inductive.add_inductive_global (serial ())
                 {quiet_mode = false, verbose = false, kind = Thm.internalK,
                   alt_name = Binding.empty, coind = false, no_elim = false,
                   no_ind = false, skip_mono = false, fork_mono = false}
-                (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (distinct (op =) (map dest_Free preds)))
+                (map (fn (s, T) =>
+                  ((Binding.name s, T), NoSyn)) (distinct (op =) (map dest_Free preds)))
                 pnames
                 (map (fn x => (Attrib.empty_binding, x)) intr_ts)
-                [] thy
+                []
+              ||> Sign.restore_naming thy
             val prednames = map (fst o dest_Const) (#preds ind_result)
             (* val rewr_thms = map mk_rewr_eq ((distinct (op =) funs) ~~ (#preds ind_result)) *)
             (* add constants to my table *)
diff -r 9290fbf0a30e -r 810c16155233 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Wed Oct 28 12:21:38 2009 +0000
+++ b/src/HOL/Tools/inductive.ML	Wed Oct 28 17:45:53 2009 +0100
@@ -592,7 +592,7 @@
 (** specification of (co)inductive predicates **)
 
 fun mk_ind_def quiet_mode skip_mono fork_mono alt_name coind cs intr_ts monos params cnames_syn ctxt =
-  let
+  let  (* FIXME proper naming convention: lthy *)
     val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp};
 
     val argTs = fold (combine (op =) o arg_types_of (length params)) cs [];
@@ -649,30 +649,37 @@
         Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn))
       else alt_name;
 
-    val ((rec_const, (_, fp_def)), ctxt') = ctxt |>
-      LocalTheory.define Thm.internalK
+    val ((rec_const, (_, fp_def)), ctxt') = ctxt
+      |> LocalTheory.conceal
+      |> LocalTheory.define Thm.internalK
         ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
          (Attrib.empty_binding, fold_rev lambda params
-           (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)));
+           (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
+      ||> LocalTheory.restore_naming ctxt;
     val fp_def' = Simplifier.rewrite (HOL_basic_ss addsimps [fp_def])
       (cterm_of (ProofContext.theory_of ctxt') (list_comb (rec_const, params)));
-    val specs = if length cs < 2 then [] else
-      map_index (fn (i, (name_mx, c)) =>
-        let
-          val Ts = arg_types_of (length params) c;
-          val xs = map Free (Variable.variant_frees ctxt intr_ts
-            (mk_names "x" (length Ts) ~~ Ts))
-        in
-          (name_mx, (Attrib.empty_binding, fold_rev lambda (params @ xs)
-            (list_comb (rec_const, params @ make_bool_args' bs i @
-              make_args argTs (xs ~~ Ts)))))
-        end) (cnames_syn ~~ cs);
-    val (consts_defs, ctxt'') = fold_map (LocalTheory.define Thm.internalK) specs ctxt';
+    val specs =
+      if length cs < 2 then []
+      else
+        map_index (fn (i, (name_mx, c)) =>
+          let
+            val Ts = arg_types_of (length params) c;
+            val xs = map Free (Variable.variant_frees ctxt intr_ts
+              (mk_names "x" (length Ts) ~~ Ts))
+          in
+            (name_mx, (Attrib.empty_binding, fold_rev lambda (params @ xs)
+              (list_comb (rec_const, params @ make_bool_args' bs i @
+                make_args argTs (xs ~~ Ts)))))
+          end) (cnames_syn ~~ cs);
+    val (consts_defs, ctxt'') = ctxt'
+      |> LocalTheory.conceal
+      |> fold_map (LocalTheory.define Thm.internalK) specs
+      ||> LocalTheory.restore_naming ctxt';
     val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
 
     val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos ctxt'';
     val ((_, [mono']), ctxt''') =
-      LocalTheory.note Thm.internalK (Attrib.empty_binding, [mono]) ctxt'';
+      LocalTheory.note Thm.internalK (apfst Binding.conceal Attrib.empty_binding, [mono]) ctxt'';
 
   in (ctxt''', rec_name, mono', fp_def', map (#2 o #2) consts_defs,
     list_comb (rec_const, params), preds, argTs, bs, xs)
@@ -697,7 +704,8 @@
     val (intrs', ctxt1) =
       ctxt |>
       LocalTheory.notes kind
-        (map (rec_qualified false) intr_bindings ~~ intr_atts ~~ map (fn th => [([th],
+        (map (rec_qualified false) intr_bindings ~~ intr_atts ~~
+          map (fn th => [([th],
            [Attrib.internal (K (ContextRules.intro_query NONE)),
             Attrib.internal (K Nitpick_Intros.add)])]) intrs) |>>
       map (hd o snd);
diff -r 9290fbf0a30e -r 810c16155233 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Wed Oct 28 12:21:38 2009 +0000
+++ b/src/HOL/Tools/inductive_set.ML	Wed Oct 28 17:45:53 2009 +0100
@@ -407,7 +407,7 @@
 fun add_ind_set_def
     {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
     cs intros monos params cnames_syn ctxt =
-  let
+  let (* FIXME proper naming convention: lthy *)
     val thy = ProofContext.theory_of ctxt;
     val {set_arities, pred_arities, to_pred_simps, ...} =
       PredSetConvData.get (Context.Proof ctxt);
@@ -419,7 +419,8 @@
     val new_arities = filter_out
       (fn (x as Free (_, T), _) => x mem params andalso length (binder_types T) > 1
         | _ => false) (fold (snd #> infer) intros []);
-    val params' = map (fn x => (case AList.lookup op = new_arities x of
+    val params' = map (fn x =>
+      (case AList.lookup op = new_arities x of
         SOME fs =>
           let
             val T = HOLogic.dest_setT (fastype_of x);
@@ -482,11 +483,14 @@
         cs' intros' monos' params1 cnames_syn' ctxt;
 
     (* define inductive sets using previously defined predicates *)
-    val (defs, ctxt2) = fold_map (LocalTheory.define Thm.internalK)
-      (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
-         fold_rev lambda params (HOLogic.Collect_const U $
-           HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
-         (cnames_syn ~~ cs_info ~~ preds)) ctxt1;
+    val (defs, ctxt2) = ctxt1
+      |> LocalTheory.conceal  (* FIXME ?? *)
+      |> fold_map (LocalTheory.define Thm.internalK)
+        (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
+           fold_rev lambda params (HOLogic.Collect_const U $
+             HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
+           (cnames_syn ~~ cs_info ~~ preds))
+      ||> LocalTheory.restore_naming ctxt1;
 
     (* prove theorems for converting predicate to set notation *)
     val ctxt3 = fold
diff -r 9290fbf0a30e -r 810c16155233 src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Wed Oct 28 12:21:38 2009 +0000
+++ b/src/HOL/Tools/quickcheck_generators.ML	Wed Oct 28 17:45:53 2009 +0100
@@ -84,7 +84,7 @@
     thy
     |> TheoryTarget.instantiation ([tyco], vs, @{sort random})
     |> `(fn lthy => Syntax.check_term lthy eq)
-    |-> (fn eq => Specification.definition (NONE, (apfst (Binding.conceal) Attrib.empty_binding, eq)))
+    |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
     |> snd
     |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
   end;
@@ -177,7 +177,7 @@
         val proj_eqs = map2 (fn v => fn proj => (v, lambda arg proj)) vs projs;
         val proj_defs = map2 (fn Free (name, _) => fn (_, rhs) =>
           ((Binding.conceal (Binding.name name), NoSyn),
-            (apfst (Binding.conceal) Attrib.empty_binding, rhs))) vs proj_eqs;
+            (apfst Binding.conceal Attrib.empty_binding, rhs))) vs proj_eqs;
         val aux_eq' = Pattern.rewrite_term thy proj_eqs [] aux_eq;
         fun prove_eqs aux_simp proj_defs lthy = 
           let
@@ -305,7 +305,7 @@
     |> random_aux_specification prfx random_auxN auxs_eqs
     |> `(fn lthy => map (Syntax.check_term lthy) random_defs)
     |-> (fn random_defs' => fold_map (fn random_def =>
-          Specification.definition (NONE, (apfst (Binding.conceal)
+          Specification.definition (NONE, (apfst Binding.conceal
             Attrib.empty_binding, random_def))) random_defs')
     |> snd
     |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
diff -r 9290fbf0a30e -r 810c16155233 src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Wed Oct 28 12:21:38 2009 +0000
+++ b/src/HOL/Tools/recdef.ML	Wed Oct 28 17:45:53 2009 +0100
@@ -263,8 +263,9 @@
       error ("No termination condition #" ^ string_of_int i ^
         " in recdef definition of " ^ quote name);
   in
-    Specification.theorem Thm.internalK NONE (K I) (Binding.name bname, atts)
-      [] (Element.Shows [(Attrib.empty_binding, [(HOLogic.mk_Trueprop tc, [])])]) int lthy
+    Specification.theorem Thm.internalK NONE (K I)
+      (Binding.conceal (Binding.name bname), atts) []
+      (Element.Shows [(Attrib.empty_binding, [(HOLogic.mk_Trueprop tc, [])])]) int lthy
   end;
 
 val recdef_tc = gen_recdef_tc Attrib.intern_src Sign.intern_const;
diff -r 9290fbf0a30e -r 810c16155233 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Wed Oct 28 12:21:38 2009 +0000
+++ b/src/Pure/General/name_space.ML	Wed Oct 28 17:45:53 2009 +0100
@@ -40,6 +40,7 @@
   val root_path: naming -> naming
   val parent_path: naming -> naming
   val mandatory_path: string -> naming -> naming
+  val transform_binding: naming -> binding -> binding
   val full_name: naming -> binding -> string
   val external_names: naming -> string -> string list
   val declare: bool -> naming -> binding -> T -> string * T
@@ -254,14 +255,17 @@
 
 (* full name *)
 
+fun transform_binding (Naming {conceal = true, ...}) = Binding.conceal
+  | transform_binding _ = I;
+
 fun err_bad binding = error ("Bad name binding " ^ quote (Binding.str_of binding));
 
-fun name_spec (Naming {conceal = conceal1, path, ...}) binding =
+fun name_spec (naming as Naming {path, ...}) raw_binding =
   let
-    val (conceal2, prefix, name) = Binding.dest binding;
+    val binding = transform_binding naming raw_binding;
+    val (concealed, prefix, name) = Binding.dest binding;
     val _ = Long_Name.is_qualified name andalso err_bad binding;
 
-    val concealed = conceal1 orelse conceal2;
     val spec1 = maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix);
     val spec2 = if name = "" then [] else [(name, true)];
     val spec = spec1 @ spec2;
diff -r 9290fbf0a30e -r 810c16155233 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Wed Oct 28 12:21:38 2009 +0000
+++ b/src/Pure/Isar/expression.ML	Wed Oct 28 17:45:53 2009 +0100
@@ -641,7 +641,8 @@
       |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
       |> Sign.declare_const ((bname, predT), NoSyn) |> snd
       |> PureThy.add_defs false
-        [((Binding.map_name Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])];
+        [((Binding.conceal (Binding.map_name Thm.def_name bname), Logic.mk_equals (head, body)),
+          [Thm.kind_internal])];
     val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
 
     val cert = Thm.cterm_of defs_thy;
@@ -682,7 +683,7 @@
             thy'
             |> Sign.mandatory_path (Binding.name_of aname)
             |> PureThy.note_thmss Thm.internalK
-              [((Binding.name introN, []), [([intro], [Locale.unfold_add])])]
+              [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.unfold_add])])]
             ||> Sign.restore_naming thy';
           in (SOME statement, SOME intro, axioms, thy'') end;
     val (b_pred, b_intro, b_axioms, thy'''') =
@@ -696,8 +697,8 @@
             thy'''
             |> Sign.mandatory_path (Binding.name_of pname)
             |> PureThy.note_thmss Thm.internalK
-                 [((Binding.name introN, []), [([intro], [Locale.intro_add])]),
-                  ((Binding.name axiomsN, []),
+                 [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.intro_add])]),
+                  ((Binding.conceal (Binding.name axiomsN), []),
                     [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
             ||> Sign.restore_naming thy''';
         in (SOME statement, SOME intro, axioms, thy'''') end;
@@ -753,10 +754,10 @@
     val asm = if is_some b_statement then b_statement else a_statement;
 
     val notes =
-      if is_some asm
-      then [(Thm.internalK, [((Binding.suffix_name ("_" ^ axiomsN) bname, []),
-        [([Assumption.assume (cterm_of thy' (the asm))],
-          [(Attrib.internal o K) Locale.witness_add])])])]
+      if is_some asm then
+        [(Thm.internalK, [((Binding.conceal (Binding.suffix_name ("_" ^ axiomsN) bname), []),
+          [([Assumption.assume (cterm_of thy' (the asm))],
+            [(Attrib.internal o K) Locale.witness_add])])])]
       else [];
 
     val notes' = body_elems |>
diff -r 9290fbf0a30e -r 810c16155233 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Wed Oct 28 12:21:38 2009 +0000
+++ b/src/Pure/Isar/local_theory.ML	Wed Oct 28 17:45:53 2009 +0100
@@ -15,6 +15,7 @@
   val map_naming: (Name_Space.naming -> Name_Space.naming) -> local_theory -> local_theory
   val conceal: local_theory -> local_theory
   val set_group: serial -> local_theory -> local_theory
+  val restore_naming: local_theory -> local_theory -> local_theory
   val target_of: local_theory -> Proof.context
   val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
   val raw_theory: (theory -> theory) -> local_theory -> local_theory
@@ -24,6 +25,8 @@
   val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
   val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
   val map_contexts: (Context.generic -> Context.generic) -> local_theory -> local_theory
+  val standard_morphism: local_theory -> Proof.context -> morphism
+  val target_morphism: local_theory -> morphism
   val pretty: local_theory -> Pretty.T list
   val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory
@@ -36,7 +39,6 @@
   val term_syntax: declaration -> local_theory -> local_theory
   val declaration: declaration -> local_theory -> local_theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
-  val target_morphism: local_theory -> morphism
   val init: string -> operations -> Proof.context -> local_theory
   val restore: local_theory -> local_theory
   val reinit: local_theory -> local_theory
@@ -111,6 +113,8 @@
 val conceal = map_naming Name_Space.conceal;
 val set_group = map_naming o Name_Space.set_group;
 
+val restore_naming = map_naming o K o naming_of;
+
 
 (* target *)
 
@@ -163,6 +167,15 @@
   Context.proof_map f;
 
 
+(* morphisms *)
+
+fun standard_morphism lthy ctxt =
+  ProofContext.norm_export_morphism lthy ctxt $>
+  Morphism.binding_morphism (Name_Space.transform_binding (naming_of lthy));
+
+fun target_morphism lthy = standard_morphism lthy (target_of lthy);
+
+
 (* basic operations *)
 
 fun operation f lthy = f (#operations (get_lthy lthy)) lthy;
@@ -179,9 +192,6 @@
 
 fun note kind (a, ths) = notes kind [(a, [(ths, [])])] #>> the_single;
 
-fun target_morphism lthy =
-  ProofContext.norm_export_morphism lthy (target_of lthy);
-
 fun notation add mode raw_args lthy =
   let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args
   in term_syntax (ProofContext.target_notation add mode args) lthy end;
@@ -215,14 +225,14 @@
 fun exit_result f (x, lthy) =
   let
     val ctxt = exit lthy;
-    val phi = ProofContext.norm_export_morphism lthy ctxt;
+    val phi = standard_morphism lthy ctxt;
   in (f phi x, ctxt) end;
 
 fun exit_result_global f (x, lthy) =
   let
     val thy = exit_global lthy;
     val thy_ctxt = ProofContext.init thy;
-    val phi = ProofContext.norm_export_morphism lthy thy_ctxt;
+    val phi = standard_morphism lthy thy_ctxt;
   in (f phi x, thy) end;
 
 end;
diff -r 9290fbf0a30e -r 810c16155233 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Oct 28 12:21:38 2009 +0000
+++ b/src/Pure/Isar/locale.ML	Wed Oct 28 17:45:53 2009 +0100
@@ -553,7 +553,8 @@
 fun add_decls add loc decl =
   ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, stamp ()))) #>
   add_thmss loc Thm.internalK
-    [((Binding.empty, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
+    [((Binding.conceal Binding.empty, [Attrib.internal (decl_attrib decl)]),
+      [([Drule.dummy_thm], [])])];
 
 in
 
diff -r 9290fbf0a30e -r 810c16155233 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Wed Oct 28 12:21:38 2009 +0000
+++ b/src/Pure/Isar/theory_target.ML	Wed Oct 28 17:45:53 2009 +0100
@@ -181,9 +181,10 @@
     val similar_body = Type.similar_types (rhs, rhs');
     (* FIXME workaround based on educated guess *)
     val prefix' = Binding.prefix_of b';
-    val class_global = Binding.eq_name (b, b')
-      andalso not (null prefix')
-      andalso (fst o snd o split_last) prefix' = Class_Target.class_prefix target;
+    val class_global =
+      Binding.eq_name (b, b') andalso
+      not (null prefix') andalso
+      fst (snd (split_last prefix')) = Class_Target.class_prefix target;
   in
     not (is_class andalso (similar_body orelse class_global)) ?
       (Context.mapping_result
@@ -202,7 +203,7 @@
     val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
     val U = map #2 xs ---> T;
     val (mx1, mx2, mx3) = fork_mixfix ta mx;
-    val declare_const =
+    val (const, lthy') = lthy |>
       (case Class_Target.instantiation_param lthy b of
         SOME c' =>
           if mx3 <> NoSyn then syntax_error c'
@@ -215,7 +216,6 @@
                 else LocalTheory.theory_result (Overloading.declare (c', U))
                   ##> Overloading.confirm b
             | NONE => LocalTheory.theory_result (Sign.declare_const ((b, U), mx3))));
-    val (const, lthy') = lthy |> declare_const;
     val t = Term.list_comb (const, map Free xs);
   in
     lthy'
@@ -275,13 +275,13 @@
 
     (*def*)
     val (global_def, lthy3) = lthy2
-      |> LocalTheory.theory_result (case Overloading.operation lthy b of
-          SOME (_, checked) =>
-            Overloading.define checked name' ((fst o dest_Const) lhs', rhs')
+      |> LocalTheory.theory_result
+        (case Overloading.operation lthy b of
+          SOME (_, checked) => Overloading.define checked name' (fst (dest_Const lhs'), rhs')
         | NONE =>
             if is_none (Class_Target.instantiation_param lthy b)
             then Thm.add_def false false (name', Logic.mk_equals (lhs', rhs'))
-            else AxClass.define_overloaded name' ((fst o dest_Const) lhs', rhs'));
+            else AxClass.define_overloaded name' (fst (dest_Const lhs'), rhs'));
     val def = LocalDefs.trans_terms lthy3
       [(*c == global.c xs*)     local_def,
        (*global.c xs == rhs'*)  global_def,
@@ -341,6 +341,9 @@
 fun context "-" thy = init NONE thy
   | context target thy = init (SOME (Locale.intern thy target)) thy;
 
+
+(* other targets *)
+
 fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []);
 fun instantiation_cmd raw_arities thy =
   instantiation (Class_Target.read_multi_arity thy raw_arities) thy;
diff -r 9290fbf0a30e -r 810c16155233 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Wed Oct 28 12:21:38 2009 +0000
+++ b/src/Pure/axclass.ML	Wed Oct 28 17:45:53 2009 +0100
@@ -311,7 +311,7 @@
         (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))
       #>> Thm.varifyT
       #-> (fn thm => add_inst_param (c, tyco) (c'', thm)
-      #> PureThy.add_thm ((Binding.name c', thm), [Thm.kind_internal])
+      #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), [Thm.kind_internal])
       #> snd
       #> Sign.restore_naming thy
       #> pair (Const (c, T))))
diff -r 9290fbf0a30e -r 810c16155233 src/Pure/conjunction.ML
--- a/src/Pure/conjunction.ML	Wed Oct 28 12:21:38 2009 +0000
+++ b/src/Pure/conjunction.ML	Wed Oct 28 17:45:53 2009 +0100
@@ -83,15 +83,16 @@
 
 in
 
-val conjunctionD1 = Drule.store_standard_thm "conjunctionD1" (conjunctionD #1);
-val conjunctionD2 = Drule.store_standard_thm "conjunctionD2" (conjunctionD #2);
+val conjunctionD1 = Drule.store_standard_thm (Binding.name "conjunctionD1") (conjunctionD #1);
+val conjunctionD2 = Drule.store_standard_thm (Binding.name "conjunctionD2") (conjunctionD #2);
 
-val conjunctionI = Drule.store_standard_thm "conjunctionI"
-  (Drule.implies_intr_list [A, B]
-    (Thm.equal_elim
-      (Thm.symmetric conjunction_def)
-      (Thm.forall_intr C (Thm.implies_intr ABC
-        (Drule.implies_elim_list (Thm.assume ABC) [Thm.assume A, Thm.assume B])))));
+val conjunctionI =
+  Drule.store_standard_thm (Binding.name "conjunctionI")
+    (Drule.implies_intr_list [A, B]
+      (Thm.equal_elim
+        (Thm.symmetric conjunction_def)
+        (Thm.forall_intr C (Thm.implies_intr ABC
+          (Drule.implies_elim_list (Thm.assume ABC) [Thm.assume A, Thm.assume B])))));
 
 
 fun intr tha thb =
diff -r 9290fbf0a30e -r 810c16155233 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Wed Oct 28 12:21:38 2009 +0000
+++ b/src/Pure/drule.ML	Wed Oct 28 17:45:53 2009 +0100
@@ -78,10 +78,10 @@
   val standard: thm -> thm
   val standard': thm -> thm
   val get_def: theory -> xstring -> thm
-  val store_thm: bstring -> thm -> thm
-  val store_standard_thm: bstring -> thm -> thm
-  val store_thm_open: bstring -> thm -> thm
-  val store_standard_thm_open: bstring -> thm -> thm
+  val store_thm: binding -> thm -> thm
+  val store_standard_thm: binding -> thm -> thm
+  val store_thm_open: binding -> thm -> thm
+  val store_standard_thm_open: binding -> thm -> thm
   val compose_single: thm * int * thm -> thm
   val imp_cong_rule: thm -> thm -> thm
   val arg_cong_rule: cterm -> thm -> thm
@@ -455,27 +455,32 @@
 fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name;
 
 fun store_thm name th =
-  Context.>>> (Context.map_theory_result (PureThy.store_thm (Binding.name name, th)));
+  Context.>>> (Context.map_theory_result (PureThy.store_thm (name, th)));
 
 fun store_thm_open name th =
-  Context.>>> (Context.map_theory_result (PureThy.store_thm_open (Binding.name name, th)));
+  Context.>>> (Context.map_theory_result (PureThy.store_thm_open (name, th)));
 
 fun store_standard_thm name th = store_thm name (standard th);
 fun store_standard_thm_open name thm = store_thm_open name (standard' thm);
 
 val reflexive_thm =
   let val cx = certify (Var(("x",0),TVar(("'a",0),[])))
-  in store_standard_thm_open "reflexive" (Thm.reflexive cx) end;
+  in store_standard_thm_open (Binding.name "reflexive") (Thm.reflexive cx) end;
 
 val symmetric_thm =
-  let val xy = read_prop "x::'a == y::'a"
-  in store_standard_thm_open "symmetric" (Thm.implies_intr xy (Thm.symmetric (Thm.assume xy))) end;
+  let
+    val xy = read_prop "x::'a == y::'a";
+    val thm = Thm.implies_intr xy (Thm.symmetric (Thm.assume xy));
+  in store_standard_thm_open (Binding.name "symmetric") thm end;
 
 val transitive_thm =
-  let val xy = read_prop "x::'a == y::'a"
-      val yz = read_prop "y::'a == z::'a"
-      val xythm = Thm.assume xy and yzthm = Thm.assume yz
-  in store_standard_thm_open "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
+  let
+    val xy = read_prop "x::'a == y::'a";
+    val yz = read_prop "y::'a == z::'a";
+    val xythm = Thm.assume xy;
+    val yzthm = Thm.assume yz;
+    val thm = Thm.implies_intr yz (Thm.transitive xythm yzthm);
+  in store_standard_thm_open (Binding.name "transitive") thm end;
 
 fun symmetric_fun thm = thm RS symmetric_thm;
 
@@ -485,7 +490,8 @@
   in equal_elim (eta_conversion (cprop_of eq')) eq' end;
 
 val equals_cong =
-  store_standard_thm_open "equals_cong" (Thm.reflexive (read_prop "x::'a == y::'a"));
+  store_standard_thm_open (Binding.name "equals_cong")
+    (Thm.reflexive (read_prop "x::'a == y::'a"));
 
 val imp_cong =
   let
@@ -494,7 +500,7 @@
     val AC = read_prop "A ==> C"
     val A = read_prop "A"
   in
-    store_standard_thm_open "imp_cong" (implies_intr ABC (equal_intr
+    store_standard_thm_open (Binding.name "imp_cong") (implies_intr ABC (equal_intr
       (implies_intr AB (implies_intr A
         (equal_elim (implies_elim (assume ABC) (assume A))
           (implies_elim (assume AB) (assume A)))))
@@ -510,11 +516,12 @@
     val A = read_prop "A"
     val B = read_prop "B"
   in
-    store_standard_thm_open "swap_prems_eq" (equal_intr
-      (implies_intr ABC (implies_intr B (implies_intr A
-        (implies_elim (implies_elim (assume ABC) (assume A)) (assume B)))))
-      (implies_intr BAC (implies_intr A (implies_intr B
-        (implies_elim (implies_elim (assume BAC) (assume B)) (assume A))))))
+    store_standard_thm_open (Binding.name "swap_prems_eq")
+      (equal_intr
+        (implies_intr ABC (implies_intr B (implies_intr A
+          (implies_elim (implies_elim (assume ABC) (assume A)) (assume B)))))
+        (implies_intr BAC (implies_intr A (implies_intr B
+          (implies_elim (implies_elim (assume BAC) (assume B)) (assume A))))))
   end;
 
 val imp_cong_rule = Thm.combination o Thm.combination (Thm.reflexive implies);
@@ -577,37 +584,41 @@
 (*** Some useful meta-theorems ***)
 
 (*The rule V/V, obtains assumption solving for eresolve_tac*)
-val asm_rl = store_standard_thm_open "asm_rl" (Thm.trivial (read_prop "?psi"));
-val _ = store_thm_open "_" asm_rl;
+val asm_rl = store_standard_thm_open (Binding.name "asm_rl") (Thm.trivial (read_prop "?psi"));
+val _ = store_thm_open (Binding.name "_") asm_rl;
 
 (*Meta-level cut rule: [| V==>W; V |] ==> W *)
 val cut_rl =
-  store_standard_thm_open "cut_rl"
+  store_standard_thm_open (Binding.name "cut_rl")
     (Thm.trivial (read_prop "?psi ==> ?theta"));
 
 (*Generalized elim rule for one conclusion; cut_rl with reversed premises:
      [| PROP V;  PROP V ==> PROP W |] ==> PROP W *)
 val revcut_rl =
-  let val V = read_prop "V"
-      and VW = read_prop "V ==> W";
+  let
+    val V = read_prop "V";
+    val VW = read_prop "V ==> W";
   in
-    store_standard_thm_open "revcut_rl"
+    store_standard_thm_open (Binding.name "revcut_rl")
       (implies_intr V (implies_intr VW (implies_elim (assume VW) (assume V))))
   end;
 
 (*for deleting an unwanted assumption*)
 val thin_rl =
-  let val V = read_prop "V"
-      and W = read_prop "W";
-  in store_standard_thm_open "thin_rl" (implies_intr V (implies_intr W (assume W))) end;
+  let
+    val V = read_prop "V";
+    val W = read_prop "W";
+    val thm = implies_intr V (implies_intr W (assume W));
+  in store_standard_thm_open (Binding.name "thin_rl") thm end;
 
 (* (!!x. PROP ?V) == PROP ?V       Allows removal of redundant parameters*)
 val triv_forall_equality =
-  let val V  = read_prop "V"
-      and QV = read_prop "!!x::'a. V"
-      and x  = certify (Free ("x", Term.aT []));
+  let
+    val V = read_prop "V";
+    val QV = read_prop "!!x::'a. V";
+    val x = certify (Free ("x", Term.aT []));
   in
-    store_standard_thm_open "triv_forall_equality"
+    store_standard_thm_open (Binding.name "triv_forall_equality")
       (equal_intr (implies_intr QV (forall_elim x (assume QV)))
         (implies_intr V  (forall_intr x (assume V))))
   end;
@@ -617,10 +628,10 @@
 *)
 val distinct_prems_rl =
   let
-    val AAB = read_prop "Phi ==> Phi ==> Psi"
+    val AAB = read_prop "Phi ==> Phi ==> Psi";
     val A = read_prop "Phi";
   in
-    store_standard_thm_open "distinct_prems_rl"
+    store_standard_thm_open (Binding.name "distinct_prems_rl")
       (implies_intr_list [AAB, A] (implies_elim_list (assume AAB) [assume A, assume A]))
   end;
 
@@ -629,15 +640,17 @@
    `thm COMP swap_prems_rl' swaps the first two premises of `thm'
 *)
 val swap_prems_rl =
-  let val cmajor = read_prop "PhiA ==> PhiB ==> Psi";
-      val major = assume cmajor;
-      val cminor1 = read_prop "PhiA";
-      val minor1 = assume cminor1;
-      val cminor2 = read_prop "PhiB";
-      val minor2 = assume cminor2;
-  in store_standard_thm_open "swap_prems_rl"
-       (implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1
-         (implies_elim (implies_elim major minor1) minor2))))
+  let
+    val cmajor = read_prop "PhiA ==> PhiB ==> Psi";
+    val major = assume cmajor;
+    val cminor1 = read_prop "PhiA";
+    val minor1 = assume cminor1;
+    val cminor2 = read_prop "PhiB";
+    val minor2 = assume cminor2;
+  in
+    store_standard_thm_open (Binding.name "swap_prems_rl")
+      (implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1
+        (implies_elim (implies_elim major minor1) minor2))))
   end;
 
 (* [| PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi |]
@@ -645,29 +658,36 @@
    Introduction rule for == as a meta-theorem.
 *)
 val equal_intr_rule =
-  let val PQ = read_prop "phi ==> psi"
-      and QP = read_prop "psi ==> phi"
+  let
+    val PQ = read_prop "phi ==> psi";
+    val QP = read_prop "psi ==> phi";
   in
-    store_standard_thm_open "equal_intr_rule"
+    store_standard_thm_open (Binding.name "equal_intr_rule")
       (implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP))))
   end;
 
 (* PROP ?phi == PROP ?psi ==> PROP ?phi ==> PROP ?psi *)
 val equal_elim_rule1 =
-  let val eq = read_prop "phi::prop == psi::prop"
-      and P = read_prop "phi"
-  in store_standard_thm_open "equal_elim_rule1"
-    (Thm.equal_elim (assume eq) (assume P) |> implies_intr_list [eq, P])
+  let
+    val eq = read_prop "phi::prop == psi::prop";
+    val P = read_prop "phi";
+  in
+    store_standard_thm_open (Binding.name "equal_elim_rule1")
+      (Thm.equal_elim (assume eq) (assume P) |> implies_intr_list [eq, P])
   end;
 
 (* PROP ?psi == PROP ?phi ==> PROP ?phi ==> PROP ?psi *)
 val equal_elim_rule2 =
-  store_standard_thm_open "equal_elim_rule2" (symmetric_thm RS equal_elim_rule1);
+  store_standard_thm_open (Binding.name "equal_elim_rule2")
+    (symmetric_thm RS equal_elim_rule1);
 
 (* PROP ?phi ==> PROP ?phi ==> PROP ?psi ==> PROP ?psi *)
 val remdups_rl =
-  let val P = read_prop "phi" and Q = read_prop "psi";
-  in store_standard_thm_open "remdups_rl" (implies_intr_list [P, P, Q] (Thm.assume Q)) end;
+  let
+    val P = read_prop "phi";
+    val Q = read_prop "psi";
+    val thm = implies_intr_list [P, P, Q] (Thm.assume Q);
+  in store_standard_thm_open (Binding.name "remdups_rl") thm end;
 
 
 
@@ -688,13 +708,18 @@
 
 val protect = Thm.capply (certify Logic.protectC);
 
-val protectI = store_thm "protectI" (Thm.kind_rule Thm.internalK (standard
-    (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A))));
+val protectI =
+  store_thm (Binding.conceal (Binding.name "protectI"))
+    (Thm.kind_rule Thm.internalK (standard
+      (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A))));
 
-val protectD = store_thm "protectD" (Thm.kind_rule Thm.internalK (standard
-    (Thm.equal_elim prop_def (Thm.assume (protect A)))));
+val protectD =
+  store_thm (Binding.conceal (Binding.name "protectD"))
+    (Thm.kind_rule Thm.internalK (standard
+      (Thm.equal_elim prop_def (Thm.assume (protect A)))));
 
-val protect_cong = store_standard_thm_open "protect_cong" (Thm.reflexive (protect A));
+val protect_cong =
+  store_standard_thm_open (Binding.name "protect_cong") (Thm.reflexive (protect A));
 
 fun implies_intr_protected asms th =
   let val asms' = map protect asms in
@@ -707,8 +732,10 @@
 
 (* term *)
 
-val termI = store_thm "termI" (Thm.kind_rule Thm.internalK (standard
-    (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A)))));
+val termI =
+  store_thm (Binding.conceal (Binding.name "termI"))
+    (Thm.kind_rule Thm.internalK (standard
+      (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A)))));
 
 fun mk_term ct =
   let
@@ -735,13 +762,17 @@
 
 (* sort_constraint *)
 
-val sort_constraintI = store_thm "sort_constraintI" (Thm.kind_rule Thm.internalK (standard
-  (Thm.equal_elim (Thm.symmetric sort_constraint_def) (mk_term T))));
+val sort_constraintI =
+  store_thm (Binding.conceal (Binding.name "sort_constraintI"))
+    (Thm.kind_rule Thm.internalK (standard
+      (Thm.equal_elim (Thm.symmetric sort_constraint_def) (mk_term T))));
 
-val sort_constraint_eq = store_thm "sort_constraint_eq" (Thm.kind_rule Thm.internalK (standard
-  (Thm.equal_intr
-    (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA) (Thm.unvarify sort_constraintI)))
-    (implies_intr_list [A, C] (Thm.assume A)))));
+val sort_constraint_eq =
+  store_thm (Binding.conceal (Binding.name "sort_constraint_eq"))
+    (Thm.kind_rule Thm.internalK (standard
+      (Thm.equal_intr
+        (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA) (Thm.unvarify sort_constraintI)))
+        (implies_intr_list [A, C] (Thm.assume A)))));
 
 end;
 
@@ -773,7 +804,7 @@
         |> Thm.forall_intr cx
         |> Thm.implies_intr cphi
         |> Thm.implies_intr rhs)
-    |> store_standard_thm_open "norm_hhf_eq"
+    |> store_standard_thm_open (Binding.name "norm_hhf_eq")
   end;
 
 val norm_hhf_prop = Logic.dest_equals (Thm.prop_of norm_hhf_eq);