# HG changeset patch # User wenzelm # Date 1456522724 -3600 # Node ID 702085ca85648014ef4b57699fb772c7bc9892db # Parent 922e702ae8ca967f4b1a293e65933cd65cea2ab9 take qualification of type name more seriously: derived consts and facts are qualified uniformly; diff -r 922e702ae8ca -r 702085ca8564 src/HOL/Import/import_rule.ML --- a/src/HOL/Import/import_rule.ML Thu Mar 03 23:33:41 2016 +0100 +++ b/src/HOL/Import/import_rule.ML Fri Feb 26 22:38:44 2016 +0100 @@ -219,8 +219,9 @@ val tfrees = Term.add_tfrees c [] val tnames = sort_strings (map fst tfrees) val typedef_bindings = - Typedef.make_morphisms (Binding.name tycname) - (SOME (Binding.name rep_name, Binding.name abs_name)) + {Rep_name = Binding.name rep_name, + Abs_name = Binding.name abs_name, + type_definition_name = Binding.name ("type_definition_" ^ tycname)} val ((_, typedef_info), thy') = Typedef.add_typedef_global {overloaded = false} (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c diff -r 922e702ae8ca -r 702085ca8564 src/HOL/Tools/hologic.ML --- a/src/HOL/Tools/hologic.ML Thu Mar 03 23:33:41 2016 +0100 +++ b/src/HOL/Tools/hologic.ML Fri Feb 26 22:38:44 2016 +0100 @@ -644,9 +644,9 @@ val literalT = Type ("String.literal", []); -fun mk_literal s = Const ("String.STR", stringT --> literalT) +fun mk_literal s = Const ("String.literal.STR", stringT --> literalT) $ mk_string s; -fun dest_literal (Const ("String.STR", _) $ t) = +fun dest_literal (Const ("String.literal.STR", _) $ t) = dest_string t | dest_literal t = raise TERM ("dest_literal", [t]); diff -r 922e702ae8ca -r 702085ca8564 src/HOL/Tools/typedef.ML --- a/src/HOL/Tools/typedef.ML Thu Mar 03 23:33:41 2016 +0100 +++ b/src/HOL/Tools/typedef.ML Fri Feb 26 22:38:44 2016 +0100 @@ -176,27 +176,30 @@ type bindings = {Rep_name: binding, Abs_name: binding, type_definition_name: binding}; +fun prefix_binding prfx name = + Binding.qualified false (prfx ^ Binding.name_of name) name; + +fun qualify_binding name = Binding.qualify false (Binding.name_of name); + fun default_bindings name = - {Rep_name = Binding.prefix_name "Rep_" name, - Abs_name = Binding.prefix_name "Abs_" name, - type_definition_name = Binding.prefix_name "type_definition_" name}; + {Rep_name = prefix_binding "Rep_" name, + Abs_name = prefix_binding "Abs_" name, + type_definition_name = prefix_binding "type_definition_" name}; fun make_bindings name NONE = default_bindings name | make_bindings _ (SOME bindings) = bindings; fun make_morphisms name NONE = default_bindings name | make_morphisms name (SOME (Rep_name, Abs_name)) = - {Rep_name = Rep_name, Abs_name = Abs_name, - type_definition_name = #type_definition_name (default_bindings name)}; + {Rep_name = qualify_binding name Rep_name, + Abs_name = qualify_binding name Abs_name, + type_definition_name = #type_definition_name (default_bindings name)}; (* prepare_typedef *) fun prepare_typedef prep_term overloaded (name, raw_args, mx) raw_set opt_bindings lthy = let - val bname = Binding.name_of name; - - (* rhs *) val tmp_ctxt = lthy |> fold (Variable.declare_typ o TFree) raw_args; @@ -207,6 +210,7 @@ val oldT = HOLogic.dest_setT setT handle TYPE _ => error ("Not a set type: " ^ quote (Syntax.string_of_typ lthy setT)); + val bname = Binding.name_of name; val goal = mk_inhabited set; val goal_pat = mk_inhabited (Var (the_default (bname, 0) (Lexicon.read_variable bname), setT)); @@ -235,8 +239,8 @@ (* result *) - fun note_qualify ((b, atts), th) = - Local_Theory.note ((Binding.qualify false bname b, map (Attrib.internal o K) atts), [th]) + fun note ((b, atts), th) = + Local_Theory.note ((b, map (Attrib.internal o K) atts), [th]) #>> (fn (_, [th']) => th'); fun typedef_result inhabited lthy1 = @@ -246,25 +250,25 @@ val (((((((((((_, [type_definition]), Rep), Rep_inverse), Abs_inverse), Rep_inject), Abs_inject), Rep_cases), Abs_cases), Rep_induct), Abs_induct), lthy2) = lthy1 |> Local_Theory.note ((type_definition_name, []), [typedef']) - ||>> note_qualify ((Rep_name, []), make @{thm type_definition.Rep}) - ||>> note_qualify ((Binding.suffix_name "_inverse" Rep_name, []), + ||>> note ((Rep_name, []), make @{thm type_definition.Rep}) + ||>> note ((Binding.suffix_name "_inverse" Rep_name, []), make @{thm type_definition.Rep_inverse}) - ||>> note_qualify ((Binding.suffix_name "_inverse" Abs_name, []), + ||>> note ((Binding.suffix_name "_inverse" Abs_name, []), make @{thm type_definition.Abs_inverse}) - ||>> note_qualify ((Binding.suffix_name "_inject" Rep_name, []), + ||>> note ((Binding.suffix_name "_inject" Rep_name, []), make @{thm type_definition.Rep_inject}) - ||>> note_qualify ((Binding.suffix_name "_inject" Abs_name, []), + ||>> note ((Binding.suffix_name "_inject" Abs_name, []), make @{thm type_definition.Abs_inject}) - ||>> note_qualify ((Binding.suffix_name "_cases" Rep_name, + ||>> note ((Binding.suffix_name "_cases" Rep_name, [Rule_Cases.case_names [Binding.name_of Rep_name], Induct.cases_pred full_name]), make @{thm type_definition.Rep_cases}) - ||>> note_qualify ((Binding.suffix_name "_cases" Abs_name, + ||>> note ((Binding.suffix_name "_cases" Abs_name, [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.cases_type full_name]), make @{thm type_definition.Abs_cases}) - ||>> note_qualify ((Binding.suffix_name "_induct" Rep_name, + ||>> note ((Binding.suffix_name "_induct" Rep_name, [Rule_Cases.case_names [Binding.name_of Rep_name], Induct.induct_pred full_name]), make @{thm type_definition.Rep_induct}) - ||>> note_qualify ((Binding.suffix_name "_induct" Abs_name, + ||>> note ((Binding.suffix_name "_induct" Abs_name, [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.induct_type full_name]), make @{thm type_definition.Abs_induct});