dropped ancient flat_names option

--- a/src/HOL/Nominal/nominal_datatype.ML	Tue Jul 21 15:44:31 2009 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Tue Jul 21 15:52:30 2009 +0200
@@ -815,7 +815,7 @@
         val (thy', defs', eqns') = Library.foldl (make_constr_def tname T T')
           ((Sign.add_path tname thy, defs, []), constrs ~~ constrs' ~~ constr_syntax)
       in
-        (parent_path (#flat_names config) thy', defs', eqns @ [eqns'], dist_lemmas @ [dist])
+        (Sign.parent_path thy', defs', eqns @ [eqns'], dist_lemmas @ [dist])
       end;
 
     val (thy8, constr_defs, constr_rep_eqns, dist_lemmas) = Library.foldl dt_constr_defs

--- a/src/HOL/Tools/Datatype/datatype.ML	Tue Jul 21 15:44:31 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML	Tue Jul 21 15:52:30 2009 +0200
@@ -552,8 +552,7 @@
             val _ = (case fold (curry OldTerm.add_typ_tfree_names) cargs' [] \\ tvs of
                 [] => ()
               | vs => error ("Extra type variables on rhs: " ^ commas vs))
-          in (constrs @ [((if #flat_names config then Sign.full_name tmp_thy else
-                Sign.full_name_path tmp_thy tname')
+          in (constrs @ [(Sign.full_name_path tmp_thy tname'
                   (Binding.map_name (Syntax.const_name mx') cname),
                    map (dtyp_of_typ new_dts) cargs')],
               constr_syntax' @ [(cname, mx')], sorts'')

--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Tue Jul 21 15:44:31 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Tue Jul 21 15:52:30 2009 +0200
@@ -93,7 +93,7 @@
     val _ = message config "Constructing primrec combinators ...";
 
     val big_name = space_implode "_" new_type_names;
-    val thy0 = add_path (#flat_names config) big_name thy;
+    val thy0 = Sign.add_path big_name thy;
 
     val descr' = List.concat descr;
     val recTs = get_rec_types descr' sorts;
@@ -243,7 +243,7 @@
            Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
              set $ Free ("x", T) $ Free ("y", T'))))))
                (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
-      ||> parent_path (#flat_names config) 
+      ||> Sign.parent_path
       ||> Theory.checkpoint;
 
 
@@ -277,7 +277,7 @@
   let
     val _ = message config "Proving characteristic theorems for case combinators ...";
 
-    val thy1 = add_path (#flat_names config) (space_implode "_" new_type_names) thy;
+    val thy1 = Sign.add_path (space_implode "_" new_type_names) thy;
 
     val descr' = List.concat descr;
     val recTs = get_rec_types descr' sorts;
@@ -339,7 +339,7 @@
     thy2
     |> Context.the_theory o fold (fold Nitpick_Const_Simps.add_thm) case_thms
        o Context.Theory
-    |> parent_path (#flat_names config)
+    |> Sign.parent_path
     |> store_thmss "cases" new_type_names case_thms
     |-> (fn thmss => pair (thmss, case_names))
   end;

--- a/src/HOL/Tools/Datatype/datatype_aux.ML	Tue Jul 21 15:44:31 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Tue Jul 21 15:52:30 2009 +0200
@@ -22,9 +22,6 @@
 
   val message : config -> string -> unit
   
-  val add_path : bool -> string -> theory -> theory
-  val parent_path : bool -> theory -> theory
-
   val store_thmss_atts : string -> string list -> attribute list list -> thm list list
     -> theory -> thm list list * theory
   val store_thmss : string -> string list -> thm list list -> theory -> thm list list * theory
@@ -76,15 +73,12 @@
 
 (* datatype option flags *)
 
-type config = { strict: bool, flat_names: bool, quiet: bool };
+type config = { strict: bool, quiet: bool };
 val default_config : config =
-  { strict = true, flat_names = false, quiet = false };
+  { strict = true, quiet = false };
 fun message ({ quiet, ...} : config) s =
   if quiet then () else writeln s;
 
-fun add_path flat_names s = if flat_names then I else Sign.add_path s;
-fun parent_path flat_names = if flat_names then I else Sign.parent_path;
-
 
 (* store theorems in theory *)
 

--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Tue Jul 21 15:44:31 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Tue Jul 21 15:52:30 2009 +0200
@@ -66,7 +66,7 @@
     val descr' = flat descr;
 
     val big_name = space_implode "_" new_type_names;
-    val thy1 = add_path (#flat_names config) big_name thy;
+    val thy1 = Sign.add_path big_name thy;
     val big_rec_name = big_name ^ "_rep_set";
     val rep_set_names' =
       (if length descr' = 1 then [big_rec_name] else
@@ -187,7 +187,7 @@
     (********************************* typedef ********************************)
 
     val (typedefs, thy3) = thy2 |>
-      parent_path (#flat_names config) |>
+      Sign.parent_path |>
       fold_map (fn ((((name, mx), tvs), c), name') =>
           Typedef.add_typedef false (SOME (Binding.name name')) (name, tvs, mx)
             (Collect $ Const (c, UnivT')) NONE
@@ -196,7 +196,7 @@
               (resolve_tac rep_intrs 1)))
                 (types_syntax ~~ tyvars ~~
                   (Library.take (length newTs, rep_set_names)) ~~ new_type_names) ||>
-      add_path (#flat_names config) big_name;
+      Sign.add_path big_name;
 
     (*********************** definition of constructors ***********************)
 
@@ -254,14 +254,14 @@
         val cong' = standard (cterm_instantiate [(cterm_of thy cong_f, rep_const)] arg_cong);
         val dist = standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
         val (thy', defs', eqns', _) = Library.foldl ((make_constr_def tname T) (length constrs))
-          ((add_path (#flat_names config) tname thy, defs, [], 1), constrs ~~ constr_syntax)
+          ((Sign.add_path tname thy, defs, [], 1), constrs ~~ constr_syntax)
       in
-        (parent_path (#flat_names config) thy', defs', eqns @ [eqns'],
+        (Sign.parent_path thy', defs', eqns @ [eqns'],
           rep_congs @ [cong'], dist_lemmas @ [dist])
       end;
 
     val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) = Library.foldl dt_constr_defs
-      ((thy3 |> Sign.add_consts_i iso_decls |> parent_path (#flat_names config), [], [], [], []),
+      ((thy3 |> Sign.add_consts_i iso_decls |> Sign.parent_path, [], [], [], []),
         hd descr ~~ new_type_names ~~ newTs ~~ constr_syntax);
 
     (*********** isomorphisms for new types (introduced by typedef) ***********)
@@ -355,7 +355,7 @@
       in (thy', char_thms' @ char_thms) end;
 
     val (thy5, iso_char_thms) = apfst Theory.checkpoint (List.foldr make_iso_defs
-      (add_path (#flat_names config) big_name thy4, []) (tl descr));
+      (Sign.add_path big_name thy4, []) (tl descr));
 
     (* prove isomorphism properties *)
 
@@ -565,7 +565,7 @@
 
     val ((constr_inject', distinct_thms'), thy6) =
       thy5
-      |> parent_path (#flat_names config)
+      |> Sign.parent_path
       |> store_thmss "inject" new_type_names constr_inject
       ||>> store_thmss "distinct" new_type_names distinct_thms;