# HG changeset patch # User wenzelm # Date 1236782539 -3600 # Node ID e62d6ecab6ad717476d380237bc5fcbad54bf236 # Parent 9b94b1358b959b42fe0e71c7a345f912a0b0a4f1 explicit Binding.qualified_name -- prevents implicitly qualified bstring; diff -r 9b94b1358b95 -r e62d6ecab6ad src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Wed Mar 11 15:38:25 2009 +0100 +++ b/src/HOL/Nominal/nominal_inductive.ML Wed Mar 11 15:42:19 2009 +0100 @@ -575,7 +575,7 @@ Attrib.internal (K (RuleCases.consumes 1))]), strong_inducts) |> snd |> LocalTheory.notes Thm.theoremK (map (fn ((name, elim), (_, cases)) => - ((Binding.name (Long_Name.qualify (Long_Name.base_name name) "strong_cases"), + ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "strong_cases"), [Attrib.internal (K (RuleCases.case_names (map snd cases))), Attrib.internal (K (RuleCases.consumes 1))]), [([elim], [])])) (strong_cases ~~ induct_cases')) |> snd @@ -665,7 +665,7 @@ in ctxt |> LocalTheory.notes Thm.theoremK (map (fn (name, ths) => - ((Binding.name (Long_Name.qualify (Long_Name.base_name name) "eqvt"), + ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "eqvt"), [Attrib.internal (K NominalThmDecls.eqvt_add)]), [(ths, [])])) (names ~~ transp thss)) |> snd end; diff -r 9b94b1358b95 -r e62d6ecab6ad src/HOL/Tools/datatype_realizer.ML --- a/src/HOL/Tools/datatype_realizer.ML Wed Mar 11 15:38:25 2009 +0100 +++ b/src/HOL/Tools/datatype_realizer.ML Wed Mar 11 15:42:19 2009 +0100 @@ -128,8 +128,9 @@ val ind_name = Thm.get_name induction; val vs = map (fn i => List.nth (pnames, i)) is; val (thm', thy') = thy - |> Sign.absolute_path - |> PureThy.store_thm (Binding.name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm) + |> Sign.root_path + |> PureThy.store_thm + (Binding.qualified_name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm) ||> Sign.restore_naming thy; val ivs = rev (Term.add_vars (Logic.varify (DatatypeProp.make_ind [descr] sorts)) []); @@ -194,8 +195,8 @@ val exh_name = Thm.get_name exhaustion; val (thm', thy') = thy - |> Sign.absolute_path - |> PureThy.store_thm (Binding.name (exh_name ^ "_P_correctness"), thm) + |> Sign.root_path + |> PureThy.store_thm (Binding.qualified_name (exh_name ^ "_P_correctness"), thm) ||> Sign.restore_naming thy; val P = Var (("P", 0), rT' --> HOLogic.boolT); diff -r 9b94b1358b95 -r e62d6ecab6ad src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Wed Mar 11 15:38:25 2009 +0100 +++ b/src/HOL/Tools/function_package/fundef_package.ML Wed Mar 11 15:42:19 2009 +0100 @@ -1,10 +1,8 @@ (* Title: HOL/Tools/function_package/fundef_package.ML - ID: $Id$ Author: Alexander Krauss, TU Muenchen A package for general recursive function definitions. Isar commands. - *) signature FUNDEF_PACKAGE = @@ -36,7 +34,8 @@ open FundefLib open FundefCommon -fun note_theorem ((name, atts), ths) = LocalTheory.note Thm.theoremK ((Binding.name name, atts), ths) +fun note_theorem ((name, atts), ths) = + LocalTheory.note Thm.theoremK ((Binding.qualified_name name, atts), ths) fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" diff -r 9b94b1358b95 -r e62d6ecab6ad src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Wed Mar 11 15:38:25 2009 +0100 +++ b/src/HOL/Tools/inductive_package.ML Wed Mar 11 15:42:19 2009 +0100 @@ -698,7 +698,7 @@ ctxt1 |> LocalTheory.note kind ((rec_qualified (Binding.name "intros"), []), intrs') ||>> fold_map (fn (name, (elim, cases)) => - LocalTheory.note kind ((Binding.name (Long_Name.qualify (Long_Name.base_name name) "cases"), + LocalTheory.note kind ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "cases"), [Attrib.internal (K (RuleCases.case_names cases)), Attrib.internal (K (RuleCases.consumes 1)), Attrib.internal (K (Induct.cases_pred name)), diff -r 9b94b1358b95 -r e62d6ecab6ad src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Wed Mar 11 15:38:25 2009 +0100 +++ b/src/HOL/Tools/inductive_realizer.ML Wed Mar 11 15:42:19 2009 +0100 @@ -355,7 +355,7 @@ ((Binding.name (Long_Name.base_name (name_of_thm intr)), []), subst_atomic rlzpreds' (Logic.unvarify rintr))) (rintrs ~~ maps snd rss)) [] ||> - Sign.absolute_path; + Sign.root_path; val thy3 = fold (PureThy.hide_fact false o name_of_thm) (#intrs ind_info) thy3'; (** realizer for induction rule **) @@ -394,12 +394,12 @@ REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY' [K (rewrite_goals_tac rews), ObjectLogic.atomize_prems_tac, DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]); - val (thm', thy') = PureThy.store_thm (Binding.name (space_implode "_" + val (thm', thy') = PureThy.store_thm (Binding.qualified_name (space_implode "_" (Long_Name.qualify qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy; val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp))) (DatatypeAux.split_conj_thm thm'); val ([thms'], thy'') = PureThy.add_thmss - [((Binding.name (space_implode "_" + [((Binding.qualified_name (space_implode "_" (Long_Name.qualify qualifier "inducts" :: vs' @ Ps @ ["correctness"])), thms), [])] thy'; val realizers = inducts ~~ thms' ~~ rlzs ~~ rs; @@ -454,7 +454,7 @@ rewrite_goals_tac rews, REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_prems_tac THEN' DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]); - val (thm', thy') = PureThy.store_thm (Binding.name (space_implode "_" + val (thm', thy') = PureThy.store_thm (Binding.qualified_name (space_implode "_" (name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy in Extraction.add_realizers_i diff -r 9b94b1358b95 -r e62d6ecab6ad src/HOL/Tools/primrec_package.ML --- a/src/HOL/Tools/primrec_package.ML Wed Mar 11 15:38:25 2009 +0100 +++ b/src/HOL/Tools/primrec_package.ML Wed Mar 11 15:42:19 2009 +0100 @@ -260,7 +260,7 @@ |-> (fn defs => `(fn ctxt => prove_spec ctxt names1 rec_rewrites defs spec')) |-> (fn simps => fold_map (LocalTheory.note Thm.theoremK) simps) |-> (fn simps' => LocalTheory.note Thm.theoremK - ((qualify (Binding.name "simps"), simp_atts), maps snd simps')) + ((qualify (Binding.qualified_name "simps"), simp_atts), maps snd simps')) |>> snd end handle PrimrecError (msg, some_eqn) => error ("Primrec definition error:\n" ^ msg ^ (case some_eqn diff -r 9b94b1358b95 -r e62d6ecab6ad src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Wed Mar 11 15:38:25 2009 +0100 +++ b/src/Pure/Proof/extraction.ML Wed Mar 11 15:42:19 2009 +0100 @@ -732,12 +732,12 @@ val fu = Type.freeze u; val (def_thms, thy') = if t = nullt then ([], thy) else thy - |> Sign.add_consts_i [(Binding.name (extr_name s vs), fastype_of ft, NoSyn)] - |> PureThy.add_defs false [((Binding.name (extr_name s vs ^ "_def"), + |> Sign.add_consts_i [(Binding.qualified_name (extr_name s vs), fastype_of ft, NoSyn)] + |> PureThy.add_defs false [((Binding.qualified_name (extr_name s vs ^ "_def"), Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])] in thy' - |> PureThy.store_thm (Binding.name (corr_name s vs), + |> PureThy.store_thm (Binding.qualified_name (corr_name s vs), Thm.varifyT (funpow (length (OldTerm.term_vars corr_prop)) (Thm.forall_elim_var 0) (forall_intr_frees (ProofChecker.thm_of_proof thy' @@ -749,7 +749,7 @@ in thy - |> Sign.absolute_path + |> Sign.root_path |> fold_rev add_def defs |> Sign.restore_naming thy end; diff -r 9b94b1358b95 -r e62d6ecab6ad src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Wed Mar 11 15:38:25 2009 +0100 +++ b/src/Pure/Proof/proof_syntax.ML Wed Mar 11 15:42:19 2009 +0100 @@ -36,8 +36,8 @@ fun add_proof_atom_consts names thy = thy - |> Sign.absolute_path - |> Sign.add_consts_i (map (fn name => (Binding.name name, proofT, NoSyn)) names); + |> Sign.root_path + |> Sign.add_consts_i (map (fn name => (Binding.qualified_name name, proofT, NoSyn)) names); (** constants for application and abstraction **)