# HG changeset patch
# User huffman
# Date 1257198230 28800
# Node ID 609389f3ea1e427c1a477510fcd1d98185ca76d5
# Parent  45c5c3c51918ef3e6e717af3dbcb524a2766b628# Parent  62571cb5481159fd0fb167aed5a70fb61436db98
merged

diff -r 45c5c3c51918 -r 609389f3ea1e src/HOL/Library/OptionalSugar.thy
--- a/src/HOL/Library/OptionalSugar.thy	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/HOL/Library/OptionalSugar.thy	Mon Nov 02 13:43:50 2009 -0800
@@ -50,7 +50,7 @@
 (* type constraints with spacing *)
 setup {*
 let
-  val typ = SimpleSyntax.read_typ;
+  val typ = Simple_Syntax.read_typ;
   val typeT = Syntax.typeT;
   val spropT = Syntax.spropT;
 in
diff -r 45c5c3c51918 -r 609389f3ea1e src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/HOL/Tools/Function/function.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -44,12 +44,12 @@
     [Simplifier.simp_add,
      Nitpick_Psimps.add]
 
-fun note_theorem ((name, atts), ths) =
-  LocalTheory.note Thm.generatedK ((Binding.qualified_name name, atts), ths)
+fun note_theorem ((binding, atts), ths) =
+  LocalTheory.note Thm.generatedK ((binding, atts), ths)
 
 fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
 
-fun add_simps fnames post sort extra_qualify label moreatts simps lthy =
+fun add_simps fnames post sort extra_qualify label mod_binding moreatts simps lthy =
     let
       val spec = post simps
                    |> map (apfst (apsnd (fn ats => moreatts @ ats)))
@@ -62,7 +62,8 @@
       val simps_by_f = sort saved_simps
 
       fun add_for_f fname simps =
-        note_theorem ((Long_Name.qualify fname label, []), simps) #> snd
+        note_theorem ((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps)
+        #> snd
     in
       (saved_simps,
        fold2 add_for_f fnames simps_by_f lthy)
@@ -89,19 +90,22 @@
           cont (Thm.close_derivation proof)
 
           val fnames = map (fst o fst) fixes
-          val qualify = Long_Name.qualify defname
+          fun qualify n = Binding.name n
+            |> Binding.qualify true defname
+          val conceal_partial = if partials then I else Binding.conceal
+
           val addsmps = add_simps fnames post sort_cont
 
           val (((psimps', pinducts'), (_, [termination'])), lthy) =
             lthy
-            |> addsmps (Binding.qualify false "partial") "psimps"
-                 psimp_attribs psimps
-            ||> fold_option (snd oo addsmps I "simps" simp_attribs) trsimps
-            ||>> note_theorem ((qualify "pinduct",
+            |> addsmps (conceal_partial o Binding.qualify false "partial")
+                 "psimps" conceal_partial psimp_attribs psimps
+            ||> fold_option (snd oo addsmps I "simps" I simp_attribs) trsimps
+            ||>> note_theorem ((conceal_partial (qualify "pinduct"),
                    [Attrib.internal (K (Rule_Cases.case_names cnames)),
                     Attrib.internal (K (Rule_Cases.consumes 1)),
                     Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
-            ||>> note_theorem ((qualify "termination", []), [termination])
+            ||>> note_theorem ((Binding.conceal (qualify "termination"), []), [termination])
             ||> (snd o note_theorem ((qualify "cases",
                    [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases]))
             ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros
@@ -147,10 +151,11 @@
               full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
             val tsimps = map remove_domain_condition psimps
             val tinduct = map remove_domain_condition pinducts
-            val qualify = Long_Name.qualify defname;
+            fun qualify n = Binding.name n
+              |> Binding.qualify true defname
           in
             lthy
-            |> add_simps I "simps" simp_attribs tsimps |> snd
+            |> add_simps I "simps" I simp_attribs tsimps |> snd
             |> note_theorem
                ((qualify "induct",
                  [Attrib.internal (K (Rule_Cases.case_names case_names))]),
diff -r 45c5c3c51918 -r 609389f3ea1e src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/HOL/Tools/Function/function_common.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -65,8 +65,9 @@
       defname : string,
 
       (* contains no logical entities: invariant under morphisms *)
-      add_simps : (binding -> binding) -> string -> Attrib.src list -> thm list 
-                  -> local_theory -> thm list * local_theory,
+      add_simps : (binding -> binding) -> string -> (binding -> binding) ->
+        Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
+
       case_names : string list,
 
       fs : term list,
diff -r 45c5c3c51918 -r 609389f3ea1e src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/HOL/Tools/Function/mutual.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -148,7 +148,8 @@
             val ((f, (_, f_defthm)), lthy') =
               LocalTheory.define Thm.internalK
                 ((Binding.name fname, mixfix),
-                  (apfst Binding.conceal Attrib.empty_binding, Term.subst_bound (fsum, f_def))) lthy
+                  ((Binding.conceal (Binding.name (fname ^ "_def")), []),
+                  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 45c5c3c51918 -r 609389f3ea1e src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/HOL/Tools/record.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -262,7 +262,7 @@
 infixr 0 ==>;
 
 val op $$ = Term.list_comb;
-val op :== = PrimitiveDefs.mk_defpair;
+val op :== = Primitive_Defs.mk_defpair;
 val op === = Trueprop o HOLogic.mk_eq;
 val op ==> = Logic.mk_implies;
 
diff -r 45c5c3c51918 -r 609389f3ea1e src/HOL/Tools/rewrite_hol_proof.ML
--- a/src/HOL/Tools/rewrite_hol_proof.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/HOL/Tools/rewrite_hol_proof.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -15,8 +15,8 @@
 
 open Proofterm;
 
-val rews = map (pairself (ProofSyntax.proof_of_term @{theory} true) o
-    Logic.dest_equals o Logic.varify o ProofSyntax.read_term @{theory} propT)
+val rews = map (pairself (Proof_Syntax.proof_of_term @{theory} true) o
+    Logic.dest_equals o Logic.varify o Proof_Syntax.read_term @{theory} propT)
 
   (** eliminate meta-equality rules **)
 
diff -r 45c5c3c51918 -r 609389f3ea1e src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/HOL/Tools/typedef.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -115,7 +115,7 @@
         theory
         |> Sign.add_consts_i [(name, setT', NoSyn)]
         |> PureThy.add_defs false [Thm.no_attributes (apfst (Binding.name)
-            (PrimitiveDefs.mk_defpair (setC, set)))]
+            (Primitive_Defs.mk_defpair (setC, set)))]
         |-> (fn [th] => pair (SOME th))
       else (NONE, theory);
     fun contract_def NONE th = th
diff -r 45c5c3c51918 -r 609389f3ea1e src/HOL/Typerep.thy
--- a/src/HOL/Typerep.thy	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/HOL/Typerep.thy	Mon Nov 02 13:43:50 2009 -0800
@@ -29,7 +29,7 @@
     | typerep_tr' _ T ts = raise Match;
 in
   Sign.add_syntax_i
-    [("_TYPEREP", SimpleSyntax.read_typ "type => logic", Delimfix "(1TYPEREP/(1'(_')))")]
+    [("_TYPEREP", Simple_Syntax.read_typ "type => logic", Delimfix "(1TYPEREP/(1'(_')))")]
   #> Sign.add_trfuns ([], [("_TYPEREP", typerep_tr)], [], [])
   #> Sign.add_trfunsT [(@{const_syntax typerep}, typerep_tr')]
 end
diff -r 45c5c3c51918 -r 609389f3ea1e src/Pure/Isar/auto_bind.ML
--- a/src/Pure/Isar/auto_bind.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Isar/auto_bind.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -14,7 +14,7 @@
   val no_facts: (indexname * term option) list
 end;
 
-structure AutoBind: AUTO_BIND =
+structure Auto_Bind: AUTO_BIND =
 struct
 
 (** bindings **)
diff -r 45c5c3c51918 -r 609389f3ea1e src/Pure/Isar/constdefs.ML
--- a/src/Pure/Isar/constdefs.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Isar/constdefs.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -60,7 +60,7 @@
     val ctxt = ProofContext.init thy;
     val (structs, _) = prep_vars (map (fn (x, T) => (x, T, Structure)) raw_structs) ctxt;
     val (decls, thy') = fold_map (gen_constdef prep_vars prep_prop prep_att structs) specs thy;
-  in Pretty.writeln (ProofDisplay.pretty_consts ctxt (K true) decls); thy' end;
+  in Pretty.writeln (Proof_Display.pretty_consts ctxt (K true) decls); thy' end;
 
 val add_constdefs = gen_constdefs ProofContext.read_vars Syntax.read_prop Attrib.attribute;
 val add_constdefs_i = gen_constdefs ProofContext.cert_vars ProofContext.cert_prop (K I);
diff -r 45c5c3c51918 -r 609389f3ea1e src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Isar/element.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -294,7 +294,7 @@
 fun witness_local_proof after_qed cmd wit_propss goal_ctxt int =
   gen_witness_proof (fn after_qed' => fn propss =>
     Proof.map_context (K goal_ctxt)
-    #> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
+    #> Proof.local_goal (Proof_Display.print_results int) (K I) ProofContext.bind_propp_i
       cmd NONE after_qed' (map (pair Thm.empty_binding) propss))
     (fn wits => fn _ => after_qed wits) wit_propss [];
 
diff -r 45c5c3c51918 -r 609389f3ea1e src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Isar/isar_cmd.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -324,7 +324,7 @@
 val print_context = Toplevel.keep Toplevel.print_state_context;
 
 fun print_theory verbose = Toplevel.unknown_theory o
-  Toplevel.keep (Pretty.writeln o ProofDisplay.pretty_full_theory verbose o Toplevel.theory_of);
+  Toplevel.keep (Pretty.writeln o Proof_Display.pretty_full_theory verbose o Toplevel.theory_of);
 
 val print_syntax = Toplevel.unknown_context o
   Toplevel.keep (ProofContext.print_syntax o Toplevel.context_of);
@@ -346,8 +346,8 @@
 val print_theorems_theory = Toplevel.keep (fn state =>
   Toplevel.theory_of state |>
   (case Toplevel.previous_context_of state of
-    SOME prev => ProofDisplay.print_theorems_diff (ProofContext.theory_of prev)
-  | NONE => ProofDisplay.print_theorems));
+    SOME prev => Proof_Display.print_theorems_diff (ProofContext.theory_of prev)
+  | NONE => Proof_Display.print_theorems));
 
 val print_theorems = Toplevel.unknown_context o print_theorems_theory o print_theorems_proof;
 
@@ -408,7 +408,7 @@
   in Present.display_graph gr end);
 
 fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
-  ThmDeps.thm_deps (Proof.get_thmss (Toplevel.enter_proof_body state) args));
+  Thm_Deps.thm_deps (Proof.get_thmss (Toplevel.enter_proof_body state) args));
 
 
 (* find unused theorems *)
@@ -419,7 +419,7 @@
     val ctxt = Toplevel.context_of state;
     fun pretty_thm (a, th) = ProofContext.pretty_fact ctxt (a, [th]);
   in
-    ThmDeps.unused_thms
+    Thm_Deps.unused_thms
       (case opt_range of
         NONE => (Theory.parents_of thy, [thy])
       | SOME (xs, NONE) => (map ThyInfo.get_theory xs, [thy])
@@ -460,11 +460,11 @@
           val prop = Thm.full_prop_of thm;
           val prf' = Proofterm.rewrite_proof_notypes ([], []) prf;
         in
-          ProofSyntax.pretty_proof ctxt
+          Proof_Syntax.pretty_proof ctxt
             (if full then Reconstruct.reconstruct_proof thy prop prf' else prf')
         end
     | SOME args => Pretty.chunks
-        (map (ProofSyntax.pretty_proof_of (Proof.context_of state) full)
+        (map (Proof_Syntax.pretty_proof_of (Proof.context_of state) full)
           (Proof.get_thmss state args)));
 
 fun string_of_prop state s =
diff -r 45c5c3c51918 -r 609389f3ea1e src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Isar/isar_syn.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -685,7 +685,7 @@
   OuterSyntax.command "proof" "backward proof"
     (K.tag_proof K.prf_block)
     (Scan.option Method.parse >> (fn m => Toplevel.print o
-      Toplevel.actual_proof (ProofNode.applys (Proof.proof m)) o
+      Toplevel.actual_proof (Proof_Node.applys (Proof.proof m)) o
       Toplevel.skip_proof (fn i => i + 1)));
 
 
@@ -720,7 +720,7 @@
 val _ =
   OuterSyntax.command "back" "backtracking of proof command"
     (K.tag_proof K.prf_script)
-    (Scan.succeed (Toplevel.print o Toplevel.actual_proof ProofNode.back o Toplevel.skip_proof I));
+    (Scan.succeed (Toplevel.print o Toplevel.actual_proof Proof_Node.back o Toplevel.skip_proof I));
 
 
 (* nested commands *)
diff -r 45c5c3c51918 -r 609389f3ea1e src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Isar/local_defs.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -47,11 +47,11 @@
       quote (Syntax.string_of_term ctxt eq));
     val ((lhs, _), eq') = eq
       |> Sign.no_vars (Syntax.pp ctxt)
-      |> PrimitiveDefs.dest_def ctxt Term.is_Free (Variable.is_fixed ctxt) (K true)
+      |> Primitive_Defs.dest_def ctxt Term.is_Free (Variable.is_fixed ctxt) (K true)
       handle TERM (msg, _) => err msg | ERROR msg => err msg;
   in (Term.dest_Free (Term.head_of lhs), eq') end;
 
-val abs_def = PrimitiveDefs.abs_def #>> Term.dest_Free;
+val abs_def = Primitive_Defs.abs_def #>> Term.dest_Free;
 
 fun mk_def ctxt args =
   let
diff -r 45c5c3c51918 -r 609389f3ea1e src/Pure/Isar/local_syntax.ML
--- a/src/Pure/Isar/local_syntax.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Isar/local_syntax.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -21,7 +21,7 @@
   val extern_term: T -> term -> term
 end;
 
-structure LocalSyntax: LOCAL_SYNTAX =
+structure Local_Syntax: LOCAL_SYNTAX =
 struct
 
 (* datatype T *)
diff -r 45c5c3c51918 -r 609389f3ea1e src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Isar/local_theory.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -150,9 +150,9 @@
 fun target_result f lthy =
   let
     val (res, ctxt') = target_of lthy
-      |> ContextPosition.set_visible false
+      |> Context_Position.set_visible false
       |> f
-      ||> ContextPosition.restore_visible lthy;
+      ||> Context_Position.restore_visible lthy;
     val thy' = ProofContext.theory_of ctxt';
     val lthy' = lthy
       |> map_target (K ctxt')
diff -r 45c5c3c51918 -r 609389f3ea1e src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Isar/obtain.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -129,7 +129,7 @@
     val _ = Variable.warn_extra_tfrees fix_ctxt asms_ctxt;
 
     (*obtain statements*)
-    val thesisN = Name.variant xs AutoBind.thesisN;
+    val thesisN = Name.variant xs Auto_Bind.thesisN;
     val (thesis_var, thesis) = #1 (bind_judgment fix_ctxt thesisN);
 
     val asm_frees = fold Term.add_frees asm_props [];
@@ -142,7 +142,7 @@
       Term.list_all_free (parms, Logic.list_implies (asm_props, thesis))
       |> Library.curry Logic.list_rename_params xs;
     val obtain_prop =
-      Logic.list_rename_params ([AutoBind.thesisN],
+      Logic.list_rename_params ([Auto_Bind.thesisN],
         Term.list_all_free ([thesis_var], Logic.mk_implies (that_prop, thesis)));
 
     fun after_qed _ =
@@ -189,7 +189,7 @@
     val thy = ProofContext.theory_of ctxt;
     val cert = Thm.cterm_of thy;
 
-    val ((thesis_var, thesis), thesis_ctxt) = bind_judgment ctxt AutoBind.thesisN;
+    val ((thesis_var, thesis), thesis_ctxt) = bind_judgment ctxt Auto_Bind.thesisN;
     val rule =
       (case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) (Goal.init (cert thesis)) of
         NONE => raise THM ("Obtain.result: tactic failed", 0, facts)
@@ -273,7 +273,7 @@
     val ctxt = Proof.context_of state;
     val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
 
-    val (thesis_var, thesis) = #1 (bind_judgment ctxt AutoBind.thesisN);
+    val (thesis_var, thesis) = #1 (bind_judgment ctxt Auto_Bind.thesisN);
     val vars = ctxt |> prep_vars raw_vars |-> fold_map inferred_type |> fst |> polymorphic ctxt;
 
     fun guess_context raw_rule state' =
@@ -293,12 +293,12 @@
         |> Proof.fix_i (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms)
         |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm_i
           (obtain_export fix_ctxt rule (map cert ts)) [(Thm.empty_binding, asms)])
-        |> Proof.bind_terms AutoBind.no_facts
+        |> Proof.bind_terms Auto_Bind.no_facts
       end;
 
     val goal = Var (("guess", 0), propT);
     fun print_result ctxt' (k, [(s, [_, th])]) =
-      ProofDisplay.print_results int ctxt' (k, [(s, [th])]);
+      Proof_Display.print_results int ctxt' (k, [(s, [th])]);
     val before_qed = SOME (Method.primitive_text (Goal.conclude #> MetaSimplifier.norm_hhf #>
         (fn th => Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
     fun after_qed [[_, res]] =
@@ -307,7 +307,7 @@
     state
     |> Proof.enter_forward
     |> Proof.begin_block
-    |> Proof.fix_i [(Binding.name AutoBind.thesisN, NONE, NoSyn)]
+    |> Proof.fix_i [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
     |> Proof.chain_facts chain_facts
     |> Proof.local_goal print_result (K I) (apsnd (rpair I))
       "guess" before_qed after_qed [(Thm.empty_binding, [Logic.mk_term goal, goal])]
diff -r 45c5c3c51918 -r 609389f3ea1e src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Isar/proof.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -225,7 +225,7 @@
 
 fun put_facts facts =
   map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) #>
-  put_thms true (AutoBind.thisN, facts);
+  put_thms true (Auto_Bind.thisN, facts);
 
 fun these_factss more_facts (named_factss, state) =
   (named_factss, state |> put_facts (SOME (maps snd named_factss @ more_facts)));
@@ -710,7 +710,7 @@
   in
     state'
     |> assume_i assumptions
-    |> bind_terms AutoBind.no_facts
+    |> bind_terms Auto_Bind.no_facts
     |> `the_facts |-> (fn thms => note_thmss_i [((Binding.name name, []), [(thms, [])])])
   end;
 
@@ -941,7 +941,7 @@
 local
 
 fun gen_have prep_att prepp before_qed after_qed stmt int =
-  local_goal (ProofDisplay.print_results int) prep_att prepp "have" before_qed after_qed stmt;
+  local_goal (Proof_Display.print_results int) prep_att prepp "have" before_qed after_qed stmt;
 
 fun gen_show prep_att prepp before_qed after_qed stmt int state =
   let
@@ -949,14 +949,14 @@
     val rule = Unsynchronized.ref (NONE: thm option);
     fun fail_msg ctxt =
       "Local statement will fail to refine any pending goal" ::
-      (case ! rule of NONE => [] | SOME th => [ProofDisplay.string_of_rule ctxt "Failed" th])
+      (case ! rule of NONE => [] | SOME th => [Proof_Display.string_of_rule ctxt "Failed" th])
       |> cat_lines;
 
     fun print_results ctxt res =
-      if ! testing then () else ProofDisplay.print_results int ctxt res;
+      if ! testing then () else Proof_Display.print_results int ctxt res;
     fun print_rule ctxt th =
       if ! testing then rule := SOME th
-      else if int then priority (ProofDisplay.string_of_rule ctxt "Successful" th)
+      else if int then priority (Proof_Display.string_of_rule ctxt "Successful" th)
       else ();
     val test_proof =
       try (local_skip_proof true)
@@ -1026,10 +1026,10 @@
     val goal' = Thm.adjust_maxidx_thm (Thm.maxidx_of goal)
       (Drule.comp_no_flatten (goal, Thm.nprems_of goal) 1 Drule.protectI);
 
-    fun after_local' [[th]] = put_thms false (AutoBind.thisN, SOME [th]);
-    fun after_global' [[th]] = ProofContext.put_thms false (AutoBind.thisN, SOME [th]);
+    fun after_local' [[th]] = put_thms false (Auto_Bind.thisN, SOME [th]);
+    fun after_global' [[th]] = ProofContext.put_thms false (Auto_Bind.thisN, SOME [th]);
     val after_qed' = (after_local', after_global');
-    val this_name = ProofContext.full_name goal_ctxt (Binding.name AutoBind.thisN);
+    val this_name = ProofContext.full_name goal_ctxt (Binding.name Auto_Bind.thisN);
 
     val result_ctxt =
       state
diff -r 45c5c3c51918 -r 609389f3ea1e src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Isar/proof_context.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -166,7 +166,7 @@
   Ctxt of
    {mode: mode,                                       (*inner syntax mode*)
     naming: Name_Space.naming,                        (*local naming conventions*)
-    syntax: LocalSyntax.T,                            (*local syntax*)
+    syntax: Local_Syntax.T,                           (*local syntax*)
     consts: Consts.T * Consts.T,                      (*local/global consts*)
     facts: Facts.T,                                   (*local facts*)
     cases: (string * (Rule_Cases.T * bool)) list};    (*named case contexts*)
@@ -181,7 +181,7 @@
 (
   type T = ctxt;
   fun init thy =
-    make_ctxt (mode_default, local_naming, LocalSyntax.init thy,
+    make_ctxt (mode_default, local_naming, Local_Syntax.init thy,
       (Sign.consts_of thy, Sign.consts_of thy), Facts.empty, []);
 );
 
@@ -230,9 +230,9 @@
 val full_name = Name_Space.full_name o naming_of;
 
 val syntax_of = #syntax o rep_context;
-val syn_of = LocalSyntax.syn_of o syntax_of;
-val set_syntax_mode = map_syntax o LocalSyntax.set_mode;
-val restore_syntax_mode = map_syntax o LocalSyntax.restore_mode o syntax_of;
+val syn_of = Local_Syntax.syn_of o syntax_of;
+val set_syntax_mode = map_syntax o Local_Syntax.set_mode;
+val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o syntax_of;
 
 val consts_of = #1 o #consts o rep_context;
 val const_syntax_name = Consts.syntax_name o consts_of;
@@ -247,7 +247,7 @@
 (* theory transfer *)
 
 fun transfer_syntax thy =
-  map_syntax (LocalSyntax.rebuild thy) #>
+  map_syntax (Local_Syntax.rebuild thy) #>
   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
@@ -710,8 +710,8 @@
   in
     t
     |> Sign.extern_term (Consts.extern_early consts) thy
-    |> LocalSyntax.extern_term syntax
-    |> Syntax.standard_unparse_term (Consts.extern consts) ctxt (LocalSyntax.syn_of syntax)
+    |> Local_Syntax.extern_term syntax
+    |> Syntax.standard_unparse_term (Consts.extern consts) ctxt (Local_Syntax.syn_of syntax)
         (not (PureThy.old_appl_syntax thy))
   end;
 
@@ -773,8 +773,8 @@
 
 fun auto_bind f ts ctxt = ctxt |> bind_terms (map drop_schematic (f (theory_of ctxt) ts));
 
-val auto_bind_goal = auto_bind AutoBind.goal;
-val auto_bind_facts = auto_bind AutoBind.facts;
+val auto_bind_goal = auto_bind Auto_Bind.goal;
+val auto_bind_facts = auto_bind Auto_Bind.facts;
 
 
 (* match_bind(_i) *)
@@ -932,7 +932,7 @@
   let
     val pos = Binding.pos_of b;
     val name = full_name ctxt b;
-    val _ = ContextPosition.report_visible ctxt (Markup.local_fact_decl name) pos;
+    val _ = Context_Position.report_visible ctxt (Markup.local_fact_decl name) pos;
 
     val facts = PureThy.name_thmss false pos name raw_facts;
     fun app (th, attrs) x =
@@ -945,9 +945,9 @@
 
 fun put_thms do_props thms ctxt = ctxt
   |> map_naming (K local_naming)
-  |> ContextPosition.set_visible false
+  |> Context_Position.set_visible false
   |> update_thms do_props (apfst Binding.name thms)
-  |> ContextPosition.restore_visible ctxt
+  |> Context_Position.restore_visible ctxt
   |> restore_naming ctxt;
 
 end;
@@ -1029,7 +1029,7 @@
 
 fun notation add mode args ctxt =
   ctxt |> map_syntax
-    (LocalSyntax.update_modesyntax (theory_of ctxt) add mode (map_filter (const_syntax ctxt) args));
+    (Local_Syntax.update_modesyntax (theory_of ctxt) add mode (map_filter (const_syntax ctxt) args));
 
 fun target_notation add mode args phi =
   let val args' = filter (fn (t, _) => Type.similar_types (t, Morphism.term phi t)) args;
@@ -1083,9 +1083,9 @@
     val ctxt'' =
       ctxt'
       |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
-      |-> (map_syntax o LocalSyntax.add_syntax (theory_of ctxt) o map prep_mixfix);
+      |-> (map_syntax o Local_Syntax.add_syntax (theory_of ctxt) o map prep_mixfix);
     val _ = (vars ~~ xs') |> List.app (fn ((b, _, _), x') =>
-      ContextPosition.report_visible ctxt (Markup.fixed_decl x') (Binding.pos_of b));
+      Context_Position.report_visible ctxt (Markup.fixed_decl x') (Binding.pos_of b));
   in (xs', ctxt'') end;
 
 end;
@@ -1316,7 +1316,7 @@
       val prt_term = Syntax.pretty_term ctxt;
 
       (*structures*)
-      val structs = LocalSyntax.structs_of (syntax_of ctxt);
+      val structs = Local_Syntax.structs_of (syntax_of ctxt);
       val prt_structs = if null structs then []
         else [Pretty.block (Pretty.str "structures:" :: Pretty.brk 1 ::
           Pretty.commas (map Pretty.str structs))];
diff -r 45c5c3c51918 -r 609389f3ea1e src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Isar/proof_display.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -21,7 +21,7 @@
   val pretty_consts: Proof.context -> (string * typ -> bool) -> (string * typ) list -> Pretty.T
 end
 
-structure ProofDisplay: PROOF_DISPLAY =
+structure Proof_Display: PROOF_DISPLAY =
 struct
 
 (* toplevel pretty printing *)
diff -r 45c5c3c51918 -r 609389f3ea1e src/Pure/Isar/proof_node.ML
--- a/src/Pure/Isar/proof_node.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Isar/proof_node.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -15,36 +15,36 @@
   val apply: (Proof.state -> Proof.state) -> T -> T
 end;
 
-structure ProofNode: PROOF_NODE =
+structure Proof_Node: PROOF_NODE =
 struct
 
 (* datatype *)
 
-datatype T = ProofNode of
+datatype T = Proof_Node of
   (Proof.state *                (*first result*)
    Proof.state Seq.seq) *       (*alternative results*)
   int;                          (*linear proof position*)
 
-fun init st = ProofNode ((st, Seq.empty), 0);
+fun init st = Proof_Node ((st, Seq.empty), 0);
 
-fun current (ProofNode ((st, _), _)) = st;
-fun position (ProofNode (_, n)) = n;
+fun current (Proof_Node ((st, _), _)) = st;
+fun position (Proof_Node (_, n)) = n;
 
 
 (* backtracking *)
 
-fun back (ProofNode ((_, stq), n)) =
+fun back (Proof_Node ((_, stq), n)) =
   (case Seq.pull stq of
     NONE => error "back: no alternatives"
-  | SOME res => ProofNode (res, n));
+  | SOME res => Proof_Node (res, n));
 
 
 (* apply transformer *)
 
-fun applys f (ProofNode ((st, _), n)) =
+fun applys f (Proof_Node ((st, _), n)) =
   (case Seq.pull (f st) of
     NONE => error "empty result sequence -- proof command failed"
-  | SOME res => ProofNode (res, n + 1));
+  | SOME res => Proof_Node (res, n + 1));
 
 fun apply f = applys (Seq.single o f);
 
diff -r 45c5c3c51918 -r 609389f3ea1e src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Isar/specification.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -67,7 +67,7 @@
 (* diagnostics *)
 
 fun print_consts _ _ [] = ()
-  | print_consts ctxt pred cs = Pretty.writeln (ProofDisplay.pretty_consts ctxt pred cs);
+  | print_consts ctxt pred cs = Pretty.writeln (Proof_Display.pretty_consts ctxt pred cs);
 
 
 (* prepare specification *)
@@ -267,7 +267,7 @@
       ((name, map attrib atts),
         bs |> map (fn (b, more_atts) => (prep_fact lthy b, map attrib more_atts))));
     val (res, lthy') = lthy |> LocalTheory.notes kind facts;
-    val _ = ProofDisplay.print_results true lthy' ((kind, ""), res);
+    val _ = Proof_Display.print_results true lthy' ((kind, ""), res);
   in (res, lthy') end;
 
 val theorems = gen_theorems (K I) (K I);
@@ -298,7 +298,7 @@
         val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
         val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
 
-        val thesis = ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) AutoBind.thesisN;
+        val thesis = ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) Auto_Bind.thesisN;
 
         fun assume_case ((name, (vars, _)), asms) ctxt' =
           let
@@ -323,7 +323,7 @@
         val stmt = [((Binding.empty, atts), [(thesis, [])])];
 
         val (facts, goal_ctxt) = elems_ctxt
-          |> (snd o ProofContext.add_fixes [(Binding.name AutoBind.thesisN, NONE, NoSyn)])
+          |> (snd o ProofContext.add_fixes [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)])
           |> fold_map assume_case (obtains ~~ propp)
           |-> (fn ths => ProofContext.note_thmss Thm.assumptionK
                 [((Binding.name Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
@@ -357,19 +357,19 @@
         |> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
         |> (fn (res, lthy') =>
           if Binding.is_empty name andalso null atts then
-            (ProofDisplay.print_results true lthy' ((kind, ""), res); lthy')
+            (Proof_Display.print_results true lthy' ((kind, ""), res); lthy')
           else
             let
               val ([(res_name, _)], lthy'') = lthy'
                 |> LocalTheory.notes kind [((name, atts), [(maps #2 res, [])])];
-              val _ = ProofDisplay.print_results true lthy' ((kind, res_name), res);
+              val _ = Proof_Display.print_results true lthy' ((kind, res_name), res);
             in lthy'' end)
         |> after_qed results'
       end;
   in
     goal_ctxt
     |> ProofContext.note_thmss Thm.assumptionK
-      [((Binding.name AutoBind.assmsN, []), [(prems, [])])]
+      [((Binding.name Auto_Bind.assmsN, []), [(prems, [])])]
     |> snd
     |> Proof.theorem_i before_qed after_qed' (map snd stmt)
     |> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
diff -r 45c5c3c51918 -r 609389f3ea1e src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Isar/toplevel.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -72,7 +72,7 @@
   val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition
   val proofs: (Proof.state -> Proof.state Seq.seq) -> transition -> transition
   val proof: (Proof.state -> Proof.state) -> transition -> transition
-  val actual_proof: (ProofNode.T -> ProofNode.T) -> transition -> transition
+  val actual_proof: (Proof_Node.T -> Proof_Node.T) -> transition -> transition
   val skip_proof: (int -> int) -> transition -> transition
   val skip_proof_to_theory: (int -> bool) -> transition -> transition
   val get_id: transition -> string option
@@ -121,7 +121,7 @@
 datatype node =
   Theory of generic_theory * Proof.context option
     (*theory with presentation context*) |
-  Proof of ProofNode.T * ((Proof.context -> generic_theory) * generic_theory)
+  Proof of Proof_Node.T * ((Proof.context -> generic_theory) * generic_theory)
     (*proof node, finish, original theory*) |
   SkipProof of int * (generic_theory * generic_theory);
     (*proof depth, resulting theory, original theory*)
@@ -130,7 +130,7 @@
 val proof_node = fn Proof (prf, _) => SOME prf | _ => NONE;
 
 fun cases_node f _ (Theory (gthy, _)) = f gthy
-  | cases_node _ g (Proof (prf, _)) = g (ProofNode.current prf)
+  | cases_node _ g (Proof (prf, _)) = g (Proof_Node.current prf)
   | cases_node f _ (SkipProof (_, (gthy, _))) = f gthy;
 
 val context_node = cases_node Context.proof_of Proof.context_of;
@@ -148,7 +148,7 @@
 
 fun level (State (NONE, _)) = 0
   | level (State (SOME (Theory _, _), _)) = 0
-  | level (State (SOME (Proof (prf, _), _), _)) = Proof.level (ProofNode.current prf)
+  | level (State (SOME (Proof (prf, _), _), _)) = Proof.level (Proof_Node.current prf)
   | level (State (SOME (SkipProof (d, _), _), _)) = d + 1;   (*different notion of proof depth!*)
 
 fun str_of_state (State (NONE, _)) = "at top level"
@@ -184,7 +184,7 @@
 
 fun proof_position_of state =
   (case node_of state of
-    Proof (prf, _) => ProofNode.position prf
+    Proof (prf, _) => Proof_Node.position prf
   | _ => raise UNDEF);
 
 val enter_proof_body = node_case (Proof.init o Context.proof_of) Proof.enter_forward;
@@ -207,7 +207,7 @@
     NONE => []
   | SOME (Theory (gthy, _)) => if prf_only then [] else pretty_context gthy
   | SOME (Proof (prf, _)) =>
-      Proof.pretty_state (ProofNode.position prf) (ProofNode.current prf)
+      Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf)
   | SOME (SkipProof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)])
   |> Pretty.markup_chunks Markup.state |> Pretty.writeln;
 
@@ -450,7 +450,7 @@
 
 fun end_proof f = transaction (fn int =>
   (fn Proof (prf, (finish, _)) =>
-        let val state = ProofNode.current prf in
+        let val state = Proof_Node.current prf in
           if can (Proof.assert_bottom true) state then
             let
               val ctxt' = f int state;
@@ -475,7 +475,7 @@
       else ();
       if skip andalso not schematic then
         SkipProof (0, (finish gthy (Proof.global_skip_proof int prf), gthy))
-      else Proof (ProofNode.init prf, (finish gthy, gthy))
+      else Proof (Proof_Node.init prf, (finish gthy, gthy))
     end
   | _ => raise UNDEF));
 
@@ -499,12 +499,12 @@
     | _ => raise UNDEF));
 
 val present_proof = present_transaction (fn _ =>
-  (fn Proof (prf, x) => Proof (ProofNode.apply I prf, x)
+  (fn Proof (prf, x) => Proof (Proof_Node.apply I prf, x)
     | skip as SkipProof _ => skip
     | _ => raise UNDEF));
 
 fun proofs' f = transaction (fn int =>
-  (fn Proof (prf, x) => Proof (ProofNode.applys (f int) prf, x)
+  (fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x)
     | skip as SkipProof _ => skip
     | _ => raise UNDEF));
 
@@ -654,7 +654,7 @@
             Future.fork_pri ~1 (fn () =>
               let val (states, result_state) =
                 (case st' of State (SOME (Proof (_, (_, orig_gthy)), exit), prev)
-                  => State (SOME (Proof (ProofNode.init prf, (finish, orig_gthy)), exit), prev))
+                  => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy)), exit), prev))
                 |> fold_map command_result body_trs
                 ||> command (end_tr |> set_print false);
               in (states, presentation_context_of result_state) end))
diff -r 45c5c3c51918 -r 609389f3ea1e src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Proof/extraction.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -300,7 +300,7 @@
     val rtypes = map fst types;
     val eqns = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
     val thy' = add_syntax thy;
-    val rd = ProofSyntax.read_proof thy' false
+    val rd = Proof_Syntax.read_proof thy' false;
   in fn (thm, (vs, s1, s2)) =>
     let
       val name = Thm.get_name thm;
diff -r 45c5c3c51918 -r 609389f3ea1e src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Proof/proof_syntax.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -19,7 +19,7 @@
   val pretty_proof_of: Proof.context -> bool -> thm -> Pretty.T
 end;
 
-structure ProofSyntax : PROOF_SYNTAX =
+structure Proof_Syntax : PROOF_SYNTAX =
 struct
 
 open Proofterm;
diff -r 45c5c3c51918 -r 609389f3ea1e src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -658,7 +658,7 @@
         fun strings_of_thm (thy, name) =
           map (Display.string_of_thm_global thy) (PureThy.get_thms thy name)
 
-        val string_of_thy = Pretty.string_of o ProofDisplay.pretty_full_theory false
+        val string_of_thy = Pretty.string_of o Proof_Display.pretty_full_theory false
     in
         case (thyname, objtype) of
             (_, ObjTheory) => idvalue [string_of_thy (ThyInfo.get_theory name)]
diff -r 45c5c3c51918 -r 609389f3ea1e src/Pure/Syntax/simple_syntax.ML
--- a/src/Pure/Syntax/simple_syntax.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Syntax/simple_syntax.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -11,7 +11,7 @@
   val read_prop: string -> term
 end;
 
-structure SimpleSyntax: SIMPLE_SYNTAX =
+structure Simple_Syntax: SIMPLE_SYNTAX =
 struct
 
 (* scanning tokens *)
diff -r 45c5c3c51918 -r 609389f3ea1e src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Thy/thm_deps.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -10,7 +10,7 @@
   val unused_thms: theory list * theory list -> (string * thm) list
 end;
 
-structure ThmDeps: THM_DEPS =
+structure Thm_Deps: THM_DEPS =
 struct
 
 (* thm_deps *)
diff -r 45c5c3c51918 -r 609389f3ea1e src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Thy/thy_output.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -478,7 +478,7 @@
     val ctxt' = Variable.auto_fixes eq ctxt;
   in ProofContext.pretty_term_abbrev ctxt' eq end;
 
-fun pretty_prf full ctxt = ProofSyntax.pretty_proof_of ctxt full;
+fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full;
 
 fun pretty_theory ctxt name =
   (Theory.requires (ProofContext.theory_of ctxt) name "presentation"; Pretty.str name);
diff -r 45c5c3c51918 -r 609389f3ea1e src/Pure/Tools/xml_syntax.ML
--- a/src/Pure/Tools/xml_syntax.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Tools/xml_syntax.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -17,7 +17,7 @@
   val proof_of_xml: XML.tree -> Proofterm.proof
 end;
 
-structure XMLSyntax : XML_SYNTAX =
+structure XML_Syntax : XML_SYNTAX =
 struct
 
 (**** XML output ****)
diff -r 45c5c3c51918 -r 609389f3ea1e src/Pure/conjunction.ML
--- a/src/Pure/conjunction.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/conjunction.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -30,7 +30,7 @@
 (** abstract syntax **)
 
 fun certify t = Thm.cterm_of (Context.the_theory (Context.the_thread_data ())) t;
-val read_prop = certify o SimpleSyntax.read_prop;
+val read_prop = certify o Simple_Syntax.read_prop;
 
 val true_prop = certify Logic.true_prop;
 val conjunction = certify Logic.conjunction;
diff -r 45c5c3c51918 -r 609389f3ea1e src/Pure/context_position.ML
--- a/src/Pure/context_position.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/context_position.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -12,7 +12,7 @@
   val report_visible: Proof.context -> Markup.T -> Position.T -> unit
 end;
 
-structure ContextPosition: CONTEXT_POSITION =
+structure Context_Position: CONTEXT_POSITION =
 struct
 
 structure Data = ProofDataFun
diff -r 45c5c3c51918 -r 609389f3ea1e src/Pure/drule.ML
--- a/src/Pure/drule.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/drule.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -450,7 +450,7 @@
 
 (*** Meta-Rewriting Rules ***)
 
-val read_prop = certify o SimpleSyntax.read_prop;
+val read_prop = certify o Simple_Syntax.read_prop;
 
 fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name;
 
diff -r 45c5c3c51918 -r 609389f3ea1e src/Pure/primitive_defs.ML
--- a/src/Pure/primitive_defs.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/primitive_defs.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -12,7 +12,7 @@
   val mk_defpair: term * term -> string * term
 end;
 
-structure PrimitiveDefs: PRIMITIVE_DEFS =
+structure Primitive_Defs: PRIMITIVE_DEFS =
 struct
 
 fun term_kind (Const _) = "existing constant "
diff -r 45c5c3c51918 -r 609389f3ea1e src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/pure_setup.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -22,13 +22,13 @@
 toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
 toplevel_pp ["Position", "T"] "Pretty.position";
 toplevel_pp ["Binding", "binding"] "Pretty.str o quote o Binding.str_of";
-toplevel_pp ["Thm", "thm"] "ProofDisplay.pp_thm";
-toplevel_pp ["Thm", "cterm"] "ProofDisplay.pp_cterm";
-toplevel_pp ["Thm", "ctyp"] "ProofDisplay.pp_ctyp";
-toplevel_pp ["typ"] "ProofDisplay.pp_typ Pure.thy";
+toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm";
+toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm";
+toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp";
+toplevel_pp ["typ"] "Proof_Display.pp_typ Pure.thy";
 toplevel_pp ["Context", "theory"] "Context.pretty_thy";
 toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref";
-toplevel_pp ["Context", "Proof", "context"] "ProofDisplay.pp_context";
+toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
 toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast";
 toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode";
 toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident";
diff -r 45c5c3c51918 -r 609389f3ea1e src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/pure_thy.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -227,8 +227,8 @@
 
 (*** Pure theory syntax and logical content ***)
 
-val typ = SimpleSyntax.read_typ;
-val prop = SimpleSyntax.read_prop;
+val typ = Simple_Syntax.read_typ;
+val prop = Simple_Syntax.read_prop;
 
 val typeT = Syntax.typeT;
 val spropT = Syntax.spropT;
diff -r 45c5c3c51918 -r 609389f3ea1e src/Pure/sign.ML
--- a/src/Pure/sign.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/sign.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -392,7 +392,7 @@
   let val ((lhs, rhs), _) = tm
     |> no_vars (Syntax.pp ctxt)
     |> Logic.strip_imp_concl
-    |> PrimitiveDefs.dest_def ctxt Term.is_Const (K false) (K false)
+    |> Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false)
   in (Term.dest_Const (Term.head_of lhs), rhs) end
   handle TERM (msg, _) => error msg;
 
diff -r 45c5c3c51918 -r 609389f3ea1e src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/ZF/Tools/datatype_package.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -108,7 +108,7 @@
     let val ncon = length con_ty_list    (*number of constructors*)
         fun mk_def (((id,T,syn), name, args, prems), kcon) =
               (*kcon is index of constructor*)
-            PrimitiveDefs.mk_defpair (list_comb (Const (full_name name, T), args),
+            Primitive_Defs.mk_defpair (list_comb (Const (full_name name, T), args),
                         mk_inject npart kpart
                         (mk_inject ncon kcon (mk_tuple args)))
     in  ListPair.map mk_def (con_ty_list, 1 upto ncon)  end;
@@ -157,7 +157,7 @@
   val case_const = Const (case_name, case_typ);
   val case_tm = list_comb (case_const, case_args);
 
-  val case_def = PrimitiveDefs.mk_defpair
+  val case_def = Primitive_Defs.mk_defpair
     (case_tm, Balanced_Tree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_case case_lists));
 
 
@@ -232,7 +232,7 @@
   val recursor_cases = map call_recursor (flat case_lists ~~ flat recursor_lists);
 
   val recursor_def =
-      PrimitiveDefs.mk_defpair
+      Primitive_Defs.mk_defpair
         (recursor_tm,
          @{const Univ.Vrecursor} $
            absfree ("rec", @{typ i}, list_comb (case_const, recursor_cases)));
diff -r 45c5c3c51918 -r 609389f3ea1e src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Mon Nov 02 12:26:23 2009 -0800
+++ b/src/ZF/Tools/inductive_package.ML	Mon Nov 02 13:43:50 2009 -0800
@@ -156,7 +156,7 @@
   val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
 
   (*The individual sets must already be declared*)
-  val axpairs = map PrimitiveDefs.mk_defpair
+  val axpairs = map Primitive_Defs.mk_defpair
         ((big_rec_tm, fp_rhs) ::
          (case parts of
              [_] => []                        (*no mutual recursion*)