# HG changeset patch # User haftmann # Date 1248184350 -7200 # Node ID 9543210087853100f55ff1f79be700a9ae210a5a # Parent 8bac9ee4b28d79133b8f44164ccc6cdc0a9dd423 dropped ancient flat_names option diff -r 8bac9ee4b28d -r 954321008785 src/HOL/Nominal/nominal_datatype.ML --- 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 diff -r 8bac9ee4b28d -r 954321008785 src/HOL/Tools/Datatype/datatype.ML --- 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'') diff -r 8bac9ee4b28d -r 954321008785 src/HOL/Tools/Datatype/datatype_abs_proofs.ML --- 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; diff -r 8bac9ee4b28d -r 954321008785 src/HOL/Tools/Datatype/datatype_aux.ML --- 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 *) diff -r 8bac9ee4b28d -r 954321008785 src/HOL/Tools/Datatype/datatype_rep_proofs.ML --- 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;