dropped ancient flat_names option
authorhaftmann
Tue Jul 21 15:52:30 2009 +0200 (2009-07-21)
changeset 32124954321008785
parent 32123 8bac9ee4b28d
child 32125 10e1a6ea8df9
dropped ancient flat_names option
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Datatype/datatype_abs_proofs.ML
src/HOL/Tools/Datatype/datatype_aux.ML
src/HOL/Tools/Datatype/datatype_rep_proofs.ML
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Tue Jul 21 15:44:31 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Tue Jul 21 15:52:30 2009 +0200
     1.3 @@ -815,7 +815,7 @@
     1.4          val (thy', defs', eqns') = Library.foldl (make_constr_def tname T T')
     1.5            ((Sign.add_path tname thy, defs, []), constrs ~~ constrs' ~~ constr_syntax)
     1.6        in
     1.7 -        (parent_path (#flat_names config) thy', defs', eqns @ [eqns'], dist_lemmas @ [dist])
     1.8 +        (Sign.parent_path thy', defs', eqns @ [eqns'], dist_lemmas @ [dist])
     1.9        end;
    1.10  
    1.11      val (thy8, constr_defs, constr_rep_eqns, dist_lemmas) = Library.foldl dt_constr_defs
     2.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Tue Jul 21 15:44:31 2009 +0200
     2.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Tue Jul 21 15:52:30 2009 +0200
     2.3 @@ -552,8 +552,7 @@
     2.4              val _ = (case fold (curry OldTerm.add_typ_tfree_names) cargs' [] \\ tvs of
     2.5                  [] => ()
     2.6                | vs => error ("Extra type variables on rhs: " ^ commas vs))
     2.7 -          in (constrs @ [((if #flat_names config then Sign.full_name tmp_thy else
     2.8 -                Sign.full_name_path tmp_thy tname')
     2.9 +          in (constrs @ [(Sign.full_name_path tmp_thy tname'
    2.10                    (Binding.map_name (Syntax.const_name mx') cname),
    2.11                     map (dtyp_of_typ new_dts) cargs')],
    2.12                constr_syntax' @ [(cname, mx')], sorts'')
     3.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Tue Jul 21 15:44:31 2009 +0200
     3.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Tue Jul 21 15:52:30 2009 +0200
     3.3 @@ -93,7 +93,7 @@
     3.4      val _ = message config "Constructing primrec combinators ...";
     3.5  
     3.6      val big_name = space_implode "_" new_type_names;
     3.7 -    val thy0 = add_path (#flat_names config) big_name thy;
     3.8 +    val thy0 = Sign.add_path big_name thy;
     3.9  
    3.10      val descr' = List.concat descr;
    3.11      val recTs = get_rec_types descr' sorts;
    3.12 @@ -243,7 +243,7 @@
    3.13             Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
    3.14               set $ Free ("x", T) $ Free ("y", T'))))))
    3.15                 (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
    3.16 -      ||> parent_path (#flat_names config) 
    3.17 +      ||> Sign.parent_path
    3.18        ||> Theory.checkpoint;
    3.19  
    3.20  
    3.21 @@ -277,7 +277,7 @@
    3.22    let
    3.23      val _ = message config "Proving characteristic theorems for case combinators ...";
    3.24  
    3.25 -    val thy1 = add_path (#flat_names config) (space_implode "_" new_type_names) thy;
    3.26 +    val thy1 = Sign.add_path (space_implode "_" new_type_names) thy;
    3.27  
    3.28      val descr' = List.concat descr;
    3.29      val recTs = get_rec_types descr' sorts;
    3.30 @@ -339,7 +339,7 @@
    3.31      thy2
    3.32      |> Context.the_theory o fold (fold Nitpick_Const_Simps.add_thm) case_thms
    3.33         o Context.Theory
    3.34 -    |> parent_path (#flat_names config)
    3.35 +    |> Sign.parent_path
    3.36      |> store_thmss "cases" new_type_names case_thms
    3.37      |-> (fn thmss => pair (thmss, case_names))
    3.38    end;
     4.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Tue Jul 21 15:44:31 2009 +0200
     4.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Tue Jul 21 15:52:30 2009 +0200
     4.3 @@ -22,9 +22,6 @@
     4.4  
     4.5    val message : config -> string -> unit
     4.6    
     4.7 -  val add_path : bool -> string -> theory -> theory
     4.8 -  val parent_path : bool -> theory -> theory
     4.9 -
    4.10    val store_thmss_atts : string -> string list -> attribute list list -> thm list list
    4.11      -> theory -> thm list list * theory
    4.12    val store_thmss : string -> string list -> thm list list -> theory -> thm list list * theory
    4.13 @@ -76,15 +73,12 @@
    4.14  
    4.15  (* datatype option flags *)
    4.16  
    4.17 -type config = { strict: bool, flat_names: bool, quiet: bool };
    4.18 +type config = { strict: bool, quiet: bool };
    4.19  val default_config : config =
    4.20 -  { strict = true, flat_names = false, quiet = false };
    4.21 +  { strict = true, quiet = false };
    4.22  fun message ({ quiet, ...} : config) s =
    4.23    if quiet then () else writeln s;
    4.24  
    4.25 -fun add_path flat_names s = if flat_names then I else Sign.add_path s;
    4.26 -fun parent_path flat_names = if flat_names then I else Sign.parent_path;
    4.27 -
    4.28  
    4.29  (* store theorems in theory *)
    4.30  
     5.1 --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Tue Jul 21 15:44:31 2009 +0200
     5.2 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Tue Jul 21 15:52:30 2009 +0200
     5.3 @@ -66,7 +66,7 @@
     5.4      val descr' = flat descr;
     5.5  
     5.6      val big_name = space_implode "_" new_type_names;
     5.7 -    val thy1 = add_path (#flat_names config) big_name thy;
     5.8 +    val thy1 = Sign.add_path big_name thy;
     5.9      val big_rec_name = big_name ^ "_rep_set";
    5.10      val rep_set_names' =
    5.11        (if length descr' = 1 then [big_rec_name] else
    5.12 @@ -187,7 +187,7 @@
    5.13      (********************************* typedef ********************************)
    5.14  
    5.15      val (typedefs, thy3) = thy2 |>
    5.16 -      parent_path (#flat_names config) |>
    5.17 +      Sign.parent_path |>
    5.18        fold_map (fn ((((name, mx), tvs), c), name') =>
    5.19            Typedef.add_typedef false (SOME (Binding.name name')) (name, tvs, mx)
    5.20              (Collect $ Const (c, UnivT')) NONE
    5.21 @@ -196,7 +196,7 @@
    5.22                (resolve_tac rep_intrs 1)))
    5.23                  (types_syntax ~~ tyvars ~~
    5.24                    (Library.take (length newTs, rep_set_names)) ~~ new_type_names) ||>
    5.25 -      add_path (#flat_names config) big_name;
    5.26 +      Sign.add_path big_name;
    5.27  
    5.28      (*********************** definition of constructors ***********************)
    5.29  
    5.30 @@ -254,14 +254,14 @@
    5.31          val cong' = standard (cterm_instantiate [(cterm_of thy cong_f, rep_const)] arg_cong);
    5.32          val dist = standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
    5.33          val (thy', defs', eqns', _) = Library.foldl ((make_constr_def tname T) (length constrs))
    5.34 -          ((add_path (#flat_names config) tname thy, defs, [], 1), constrs ~~ constr_syntax)
    5.35 +          ((Sign.add_path tname thy, defs, [], 1), constrs ~~ constr_syntax)
    5.36        in
    5.37 -        (parent_path (#flat_names config) thy', defs', eqns @ [eqns'],
    5.38 +        (Sign.parent_path thy', defs', eqns @ [eqns'],
    5.39            rep_congs @ [cong'], dist_lemmas @ [dist])
    5.40        end;
    5.41  
    5.42      val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) = Library.foldl dt_constr_defs
    5.43 -      ((thy3 |> Sign.add_consts_i iso_decls |> parent_path (#flat_names config), [], [], [], []),
    5.44 +      ((thy3 |> Sign.add_consts_i iso_decls |> Sign.parent_path, [], [], [], []),
    5.45          hd descr ~~ new_type_names ~~ newTs ~~ constr_syntax);
    5.46  
    5.47      (*********** isomorphisms for new types (introduced by typedef) ***********)
    5.48 @@ -355,7 +355,7 @@
    5.49        in (thy', char_thms' @ char_thms) end;
    5.50  
    5.51      val (thy5, iso_char_thms) = apfst Theory.checkpoint (List.foldr make_iso_defs
    5.52 -      (add_path (#flat_names config) big_name thy4, []) (tl descr));
    5.53 +      (Sign.add_path big_name thy4, []) (tl descr));
    5.54  
    5.55      (* prove isomorphism properties *)
    5.56  
    5.57 @@ -565,7 +565,7 @@
    5.58  
    5.59      val ((constr_inject', distinct_thms'), thy6) =
    5.60        thy5
    5.61 -      |> parent_path (#flat_names config)
    5.62 +      |> Sign.parent_path
    5.63        |> store_thmss "inject" new_type_names constr_inject
    5.64        ||>> store_thmss "distinct" new_type_names distinct_thms;
    5.65