--- a/src/HOL/Nominal/nominal_inductive.ML Wed Mar 11 18:32:23 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML Wed Mar 11 19:27:48 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 18:32:23 2009 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML Wed Mar 11 19:27:48 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 18:32:23 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML Wed Mar 11 19:27:48 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 18:32:23 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML Wed Mar 11 19:27:48 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 18:32:23 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Wed Mar 11 19:27:48 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 18:32:23 2009 +0100
+++ b/src/HOL/Tools/primrec_package.ML Wed Mar 11 19:27:48 2009 +0100
@@ -259,7 +259,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/HOL/Word/Num_Lemmas.thy Wed Mar 11 18:32:23 2009 +0100
+++ b/src/HOL/Word/Num_Lemmas.thy Wed Mar 11 19:27:48 2009 +0100
@@ -11,9 +11,9 @@
lemma contentsI: "y = {x} ==> contents y = x"
unfolding contents_def by auto -- {* FIXME move *}
-lemmas split_split = prod.split [unfolded prod_case_split]
+lemmas split_split = prod.split [unfolded prod_case_split]
lemmas split_split_asm = prod.split_asm [unfolded prod_case_split]
-lemmas "split.splits" = split_split split_split_asm
+lemmas split_splits = split_split split_split_asm
lemmas funpow_0 = funpow.simps(1)
lemmas funpow_Suc = funpow.simps(2)
--- a/src/Pure/General/name_space.ML Wed Mar 11 18:32:23 2009 +0100
+++ b/src/Pure/General/name_space.ML Wed Mar 11 19:27:48 2009 +0100
@@ -36,7 +36,6 @@
val root_path: naming -> naming
val parent_path: naming -> naming
val no_base_names: naming -> naming
- val qualified_names: naming -> naming
val sticky_prefix: string -> naming -> naming
type 'a table = T * 'a Symtab.table
val bind: naming -> binding * 'a -> 'a table -> string * 'a table (*exception Symtab.DUP*)
@@ -174,53 +173,44 @@
datatype naming = Naming of
{path: (string * bool) list,
- no_base_names: bool,
- qualified_names: bool};
+ no_base_names: bool};
-fun make_naming (path, no_base_names, qualified_names) =
- Naming {path = path, no_base_names = no_base_names, qualified_names = qualified_names};
+fun make_naming (path, no_base_names) =
+ Naming {path = path, no_base_names = no_base_names};
-fun map_naming f (Naming {path, no_base_names, qualified_names}) =
- make_naming (f (path, no_base_names, qualified_names));
-
-fun path_of (Naming {path, ...}) = path;
+fun map_naming f (Naming {path, no_base_names}) =
+ make_naming (f (path, no_base_names));
(* configure naming *)
-val default_naming = make_naming ([], false, false);
+val default_naming = make_naming ([], false);
-fun add_path elems = map_naming (fn (path, no_base_names, qualified_names) =>
- (path @ map (rpair false) (Long_Name.explode elems), no_base_names, qualified_names));
+fun add_path elems = map_naming (fn (path, no_base_names) =>
+ (path @ map (rpair false) (Long_Name.explode elems), no_base_names));
-val root_path = map_naming (fn (_, no_base_names, qualified_names) =>
- ([], no_base_names, qualified_names));
+val root_path = map_naming (fn (_, no_base_names) => ([], no_base_names));
-val parent_path = map_naming (fn (path, no_base_names, qualified_names) =>
- (perhaps (try (#1 o split_last)) path, no_base_names, qualified_names));
+val parent_path = map_naming (fn (path, no_base_names) =>
+ (perhaps (try (#1 o split_last)) path, no_base_names));
-fun sticky_prefix elems = map_naming (fn (path, no_base_names, qualified_names) =>
- (path @ map (rpair true) (Long_Name.explode elems), no_base_names, qualified_names));
+fun sticky_prefix elems = map_naming (fn (path, no_base_names) =>
+ (path @ map (rpair true) (Long_Name.explode elems), no_base_names));
-val no_base_names = map_naming (fn (path, _, qualified_names) => (path, true, qualified_names));
-val qualified_names = map_naming (fn (path, no_base_names, _) => (path, no_base_names, true));
+val no_base_names = map_naming (fn (path, _) => (path, true));
(* full name *)
fun err_bad binding = error ("Bad name declaration " ^ quote (Binding.str_of binding));
-fun name_spec (Naming {path, qualified_names, ...}) binding =
+fun name_spec (Naming {path, ...}) binding =
let
val (prefix, name) = Binding.dest binding;
- val _ = not qualified_names andalso Long_Name.is_qualified name andalso err_bad binding;
+ val _ = Long_Name.is_qualified name andalso err_bad binding;
val spec1 = maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix);
- val spec2 =
- (case try split_last (Long_Name.explode name) of
- NONE => []
- | SOME (qual, base) => map (rpair false) qual @ [(base, true)]);
-
+ val spec2 = if name = "" then [] else [(name, true)];
val spec = spec1 @ spec2;
val _ =
exists (fn (a, _) => a = "" orelse a = "??" orelse exists_string (fn s => s = "\"") a) spec
--- a/src/Pure/Isar/constdefs.ML Wed Mar 11 18:32:23 2009 +0100
+++ b/src/Pure/Isar/constdefs.ML Wed Mar 11 19:27:48 2009 +0100
@@ -42,14 +42,15 @@
if c <> c' then
err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote c') []
else ());
+ val b = Binding.name c;
val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_bname thy c, T))] prop;
- val name = Binding.map_name (Thm.def_name_optional c) raw_name;
+ val name = Thm.def_binding_optional b raw_name;
val atts = map (prep_att thy) raw_atts;
val thy' =
thy
- |> Sign.add_consts_i [(Binding.name c, T, mx)]
+ |> Sign.add_consts_i [(b, T, mx)]
|> PureThy.add_defs false [((name, def), atts)]
|-> (fn [thm] => Code.add_default_eqn thm);
in ((c, T), thy') end;
--- a/src/Pure/Isar/element.ML Wed Mar 11 18:32:23 2009 +0100
+++ b/src/Pure/Isar/element.ML Wed Mar 11 19:27:48 2009 +0100
@@ -502,7 +502,7 @@
val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
let val ((c, _), t') = LocalDefs.cert_def ctxt t
- in (t', ((Binding.map_name (Thm.def_name_optional c) name, atts), [(t', ps)])) end);
+ in (t', ((Thm.def_binding_optional (Binding.name c) name, atts), [(t', ps)])) end);
val (_, ctxt') =
ctxt |> fold (Variable.auto_fixes o #1) asms
|> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
@@ -518,8 +518,8 @@
fun activate elem ctxt =
let val elem' = (map_ctxt_attrib Args.assignable o prep_facts ctxt) elem
in (elem', activate_elem elem' ctxt) end
- val (elems, ctxt') = fold_map activate raw_elems (ProofContext.qualified_names ctxt);
- in (elems |> map (map_ctxt_attrib Args.closure), ProofContext.restore_naming ctxt ctxt') end;
+ val (elems, ctxt') = fold_map activate raw_elems ctxt;
+ in (elems |> map (map_ctxt_attrib Args.closure), ctxt') end;
fun check_name name =
if Long_Name.is_qualified name then error ("Illegal qualified name: " ^ quote name)
--- a/src/Pure/Isar/expression.ML Wed Mar 11 18:32:23 2009 +0100
+++ b/src/Pure/Isar/expression.ML Wed Mar 11 19:27:48 2009 +0100
@@ -304,7 +304,7 @@
(a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
| Defines defs => Defines (defs |> map (fn ((name, atts), (t, ps)) =>
let val ((c, _), t') = LocalDefs.cert_def ctxt (close_frees t)
- in ((Binding.map_name (Thm.def_name_optional c) name, atts), (t', no_binds ps)) end))
+ in ((Thm.def_binding_optional (Binding.name c) name, atts), (t', no_binds ps)) end))
| e => e)
end;
--- a/src/Pure/Isar/local_defs.ML Wed Mar 11 18:32:23 2009 +0100
+++ b/src/Pure/Isar/local_defs.ML Wed Mar 11 19:27:48 2009 +0100
@@ -91,7 +91,7 @@
val ((bvars, mxs), specs) = defs |> split_list |>> split_list;
val ((bfacts, atts), rhss) = specs |> split_list |>> split_list;
val xs = map Binding.name_of bvars;
- val names = map2 (Binding.map_name o Thm.def_name_optional) xs bfacts;
+ val names = map2 Thm.def_binding_optional bvars bfacts;
val eqs = mk_def ctxt (xs ~~ rhss);
val lhss = map (fst o Logic.dest_equals) eqs;
in
--- a/src/Pure/Isar/local_theory.ML Wed Mar 11 18:32:23 2009 +0100
+++ b/src/Pure/Isar/local_theory.ML Wed Mar 11 19:27:48 2009 +0100
@@ -138,14 +138,12 @@
fun full_naming lthy =
Sign.naming_of (ProofContext.theory_of lthy)
- |> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy))
- |> NameSpace.qualified_names;
+ |> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy));
fun full_name naming = NameSpace.full_name (full_naming naming);
fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy
|> Sign.sticky_prefix (#theory_prefix (get_lthy lthy))
- |> Sign.qualified_names
|> f
||> Sign.restore_naming thy);
--- a/src/Pure/Isar/locale.ML Wed Mar 11 18:32:23 2009 +0100
+++ b/src/Pure/Isar/locale.ML Wed Mar 11 19:27:48 2009 +0100
@@ -107,19 +107,6 @@
datatype ctxt = datatype Element.ctxt;
-fun global_note_qualified kind facts thy = (*FIXME*)
- thy
- |> Sign.qualified_names
- |> PureThy.note_thmss kind facts
- ||> Sign.restore_naming thy;
-
-fun local_note_qualified kind facts ctxt = (*FIXME*)
- ctxt
- |> ProofContext.qualified_names
- |> ProofContext.note_thmss_i kind facts
- ||> ProofContext.restore_naming ctxt;
-
-
(*** Theory data ***)
@@ -337,7 +324,7 @@
fun init_global_elem (Notes (kind, facts)) thy =
let
val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
- in global_note_qualified kind facts' thy |> snd end
+ in PureThy.note_thmss kind facts' thy |> snd end
fun init_local_elem (Fixes fixes) ctxt = ctxt |>
ProofContext.add_fixes_i fixes |> snd
@@ -359,7 +346,7 @@
| init_local_elem (Notes (kind, facts)) ctxt =
let
val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts
- in local_note_qualified kind facts' ctxt |> snd end
+ in ProofContext.note_thmss_i kind facts' ctxt |> snd end
fun cons_elem false (Notes notes) elems = elems
| cons_elem _ elem elems = elem :: elems
@@ -452,7 +439,7 @@
let
val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
Attrib.map_facts (Attrib.attribute_i thy)
- in global_note_qualified kind args'' #> snd end)
+ in PureThy.note_thmss kind args'' #> snd end)
(get_registrations thy |> filter (fn (name, _) => name = loc)) thy))
in ctxt'' end;
--- a/src/Pure/Isar/proof_context.ML Wed Mar 11 18:32:23 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML Wed Mar 11 19:27:48 2009 +0100
@@ -98,7 +98,6 @@
val get_thm: Proof.context -> xstring -> thm
val add_path: string -> Proof.context -> Proof.context
val sticky_prefix: string -> Proof.context -> Proof.context
- val qualified_names: Proof.context -> Proof.context
val restore_naming: Proof.context -> Proof.context -> Proof.context
val reset_naming: Proof.context -> Proof.context
val note_thmss: string -> (Thm.binding * (Facts.ref * attribute list) list) list ->
@@ -947,7 +946,6 @@
val add_path = map_naming o NameSpace.add_path;
val sticky_prefix = map_naming o NameSpace.sticky_prefix;
-val qualified_names = map_naming NameSpace.qualified_names;
val restore_naming = map_naming o K o naming_of;
val reset_naming = map_naming (K local_naming);
--- a/src/Pure/Isar/specification.ML Wed Mar 11 18:32:23 2009 +0100
+++ b/src/Pure/Isar/specification.ML Wed Mar 11 19:27:48 2009 +0100
@@ -169,8 +169,7 @@
val (vars, [((raw_name, atts), [prop])]) =
fst (prep (the_list raw_var) [(raw_a, [raw_prop])] lthy);
val (((x, T), rhs), prove) = LocalDefs.derived_def lthy true prop;
- val name = Binding.map_name (Thm.def_name_optional x) raw_name;
- val var =
+ val var as (b, _) =
(case vars of
[] => (Binding.name x, NoSyn)
| [((b, _), mx)] =>
@@ -180,9 +179,12 @@
error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
Position.str_of (Binding.pos_of b));
in (b, mx) end);
- val ((lhs, (_, th)), lthy2) = lthy |> LocalTheory.define Thm.definitionK
+ val name = Thm.def_binding_optional b raw_name;
+ val ((lhs, (_, th)), lthy2) = lthy
+ |> LocalTheory.define Thm.definitionK
(var, ((Binding.suffix_name "_raw" name, []), rhs));
- val ((def_name, [th']), lthy3) = lthy2 |> LocalTheory.note Thm.definitionK
+ val ((def_name, [th']), lthy3) = lthy2
+ |> LocalTheory.note Thm.definitionK
((name, Code.add_default_eqn_attrib :: atts), [prove lthy2 th]);
val lhs' = Morphism.term (LocalTheory.target_morphism lthy3) lhs;
--- a/src/Pure/Isar/theory_target.ML Wed Mar 11 18:32:23 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML Wed Mar 11 19:27:48 2009 +0100
@@ -1,5 +1,6 @@
(* Title: Pure/Isar/theory_target.ML
Author: Makarius
+ Author: Florian Haftmann, TU Muenchen
Common theory/locale/class/instantiation/overloading targets.
*)
@@ -48,10 +49,10 @@
let
val thy = ProofContext.theory_of ctxt;
val target_name = (if is_class then "class " else "locale ") ^ Locale.extern thy target;
- val fixes = map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
- (#1 (ProofContext.inferred_fixes ctxt));
- val assumes = map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
- (Assumption.assms_of ctxt);
+ val fixes =
+ map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt));
+ val assumes =
+ map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])])) (Assumption.assms_of ctxt);
val elems =
(if null fixes then [] else [Element.Fixes fixes]) @
(if null assumes then [] else [Element.Assumes assumes]);
@@ -143,12 +144,6 @@
in (result'', result) end;
-fun note_local kind facts ctxt =
- ctxt
- |> ProofContext.qualified_names
- |> ProofContext.note_thmss_i kind facts
- ||> ProofContext.restore_naming ctxt;
-
fun notes (Target {target, is_locale, ...}) kind facts lthy =
let
val thy = ProofContext.theory_of lthy;
@@ -164,12 +159,10 @@
|> Attrib.map_facts (if is_locale then K I else Attrib.attribute_i thy);
in
lthy |> LocalTheory.theory
- (Sign.qualified_names
- #> PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd
- #> Sign.restore_naming thy)
- |> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd)
+ (PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd)
+ |> not is_locale ? LocalTheory.target (ProofContext.note_thmss_i kind global_facts #> snd)
|> is_locale ? LocalTheory.target (Locale.add_thmss target kind target_facts)
- |> note_local kind local_facts
+ |> ProofContext.note_thmss_i kind local_facts
end;
@@ -195,8 +188,8 @@
in
not (is_class andalso (similar_body orelse class_global)) ?
(Context.mapping_result
- (fn thy => thy |>
- Sign.no_base_names
+ (fn thy => thy
+ |> Sign.no_base_names
|> Sign.add_abbrev PrintMode.internal tags legacy_arg
||> Sign.restore_naming thy)
(ProofContext.add_abbrev PrintMode.internal tags arg)
@@ -210,7 +203,7 @@
fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy =
let
- val c = Binding.name_of b; (* FIXME Binding.qualified_name_of *)
+ val c = Binding.qualified_name_of b;
val tags = LocalTheory.group_position_of lthy;
val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
val U = map #2 xs ---> T;
@@ -278,8 +271,7 @@
val thy = ProofContext.theory_of lthy;
val thy_ctxt = ProofContext.init thy;
- val c = Binding.name_of b; (* FIXME Binding.qualified_name_of (!?) *)
- val name' = Binding.map_name (Thm.def_name_optional (Binding.name_of b)) name;
+ val name' = Thm.def_binding_optional b name;
val (rhs', rhs_conv) =
LocalDefs.export_cterm lthy thy_ctxt (Thm.cterm_of thy rhs) |>> Thm.term_of;
val xs = Variable.add_fixed (LocalTheory.target_of lthy) rhs' [];
@@ -290,6 +282,7 @@
val (_, lhs') = Logic.dest_equals (Thm.prop_of local_def);
(*def*)
+ val c = Binding.qualified_name_of b;
val define_const =
(case Overloading.operation lthy c of
SOME (_, checked) =>
--- a/src/Pure/Proof/extraction.ML Wed Mar 11 18:32:23 2009 +0100
+++ b/src/Pure/Proof/extraction.ML Wed Mar 11 19:27:48 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 18:32:23 2009 +0100
+++ b/src/Pure/Proof/proof_syntax.ML Wed Mar 11 19:27:48 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 **)
--- a/src/Pure/more_thm.ML Wed Mar 11 18:32:23 2009 +0100
+++ b/src/Pure/more_thm.ML Wed Mar 11 19:27:48 2009 +0100
@@ -57,6 +57,7 @@
val default_position_of: thm -> thm -> thm
val def_name: string -> string
val def_name_optional: string -> string -> string
+ val def_binding_optional: Binding.binding -> Binding.binding -> Binding.binding
val has_name_hint: thm -> bool
val get_name_hint: thm -> string
val put_name_hint: string -> thm -> thm
@@ -353,6 +354,9 @@
fun def_name_optional c "" = def_name c
| def_name_optional _ name = name;
+fun def_binding_optional b name =
+ if Binding.is_empty name then Binding.map_name def_name b else name;
+
(* unofficial theorem names *)
--- a/src/Pure/sign.ML Wed Mar 11 18:32:23 2009 +0100
+++ b/src/Pure/sign.ML Wed Mar 11 19:27:48 2009 +0100
@@ -126,8 +126,6 @@
val parent_path: theory -> theory
val sticky_prefix: string -> theory -> theory
val no_base_names: theory -> theory
- val qualified_names: theory -> theory
- val absolute_path: theory -> theory
val local_path: theory -> theory
val restore_naming: theory -> theory -> theory
val hide_class: bool -> string -> theory -> theory
@@ -623,9 +621,6 @@
val parent_path = map_naming NameSpace.parent_path;
val sticky_prefix = map_naming o NameSpace.sticky_prefix;
val no_base_names = map_naming NameSpace.no_base_names;
-val qualified_names = map_naming NameSpace.qualified_names;
-
-val absolute_path = root_path o qualified_names;
fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);