--- 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;
--- 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);
--- 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 "_"
--- 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)),
--- 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
--- 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
--- 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;
--- 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 **)