--- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Tue Mar 03 17:05:18 2009 +0100
+++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Tue Mar 03 18:33:21 2009 +0100
@@ -1010,7 +1010,7 @@
\end{picture}
\caption{Subclass relationship of monoids and groups:
before and after establishing the relationship
- \isa{group\ {\isasymsubseteq}\ monoid}; transitive edges left out.}
+ \isa{group\ {\isasymsubseteq}\ monoid}; transitive edges are left out.}
\label{fig:subclass}
\end{center}
\end{figure}
--- a/src/HOL/Nominal/nominal_inductive.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML Tue Mar 03 18:33:21 2009 +0100
@@ -546,7 +546,7 @@
Proof.theorem_i NONE (fn thss => fn ctxt =>
let
val rec_name = space_implode "_" (map Sign.base_name names);
- val rec_qualified = Binding.qualify rec_name;
+ val rec_qualified = Binding.qualify false rec_name;
val ind_case_names = RuleCases.case_names induct_cases;
val induct_cases' = InductivePackage.partition_rules' raw_induct
(intrs ~~ induct_cases);
--- a/src/HOL/Nominal/nominal_inductive2.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML Tue Mar 03 18:33:21 2009 +0100
@@ -453,7 +453,7 @@
Proof.theorem_i NONE (fn thss => fn ctxt =>
let
val rec_name = space_implode "_" (map Sign.base_name names);
- val rec_qualified = Binding.qualify rec_name;
+ val rec_qualified = Binding.qualify false rec_name;
val ind_case_names = RuleCases.case_names induct_cases;
val induct_cases' = InductivePackage.partition_rules' raw_induct
(intrs ~~ induct_cases);
--- a/src/HOL/Nominal/nominal_primrec.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML Tue Mar 03 18:33:21 2009 +0100
@@ -210,7 +210,7 @@
val def_name = Thm.def_name (Sign.base_name fname);
val rhs = singleton (Syntax.check_terms ctxt) raw_rhs;
val SOME var = get_first (fn ((b, _), mx) =>
- if Binding.base_name b = fname then SOME (b, mx) else NONE) fixes;
+ if Binding.name_of b = fname then SOME (b, mx) else NONE) fixes;
in
((var, ((Binding.name def_name, []), rhs)),
subst_bounds (rev (map Free frees), strip_abs_body rhs))
@@ -248,7 +248,7 @@
val (names_atts, spec') = split_list spec;
val eqns' = map unquantify spec'
val eqns = fold_rev (process_eqn lthy (fn v => Variable.is_fixed lthy v
- orelse exists (fn ((w, _), _) => v = Binding.base_name w) fixes)) spec' [];
+ orelse exists (fn ((w, _), _) => v = Binding.name_of w) fixes)) spec' [];
val dt_info = NominalPackage.get_nominal_datatypes (ProofContext.theory_of lthy);
val lsrs :: lsrss = maps (fn (_, (_, _, eqns)) =>
map (fn (_, (ls, _, rs, _, _)) => ls @ rs) eqns) eqns
@@ -285,7 +285,7 @@
set_group ? LocalTheory.set_group (serial_string ()) |>
fold_map (apfst (snd o snd) oo
LocalTheory.define Thm.definitionK o fst) defs';
- val qualify = Binding.qualify
+ val qualify = Binding.qualify false
(space_implode "_" (map (Sign.base_name o #1) defs));
val names_atts' = map (apfst qualify) names_atts;
val cert = cterm_of (ProofContext.theory_of lthy');
--- a/src/HOL/Tools/function_package/fundef_common.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_common.ML Tue Mar 03 18:33:21 2009 +0100
@@ -82,7 +82,7 @@
psimps, pinducts, termination, defname}) phi =
let
val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
- val name = Binding.base_name o Morphism.binding phi o Binding.name
+ val name = Binding.name_of o Morphism.binding phi o Binding.name
in
FundefCtxData { add_simps = add_simps, case_names = case_names,
fs = map term fs, R = term R, psimps = fact psimps,
--- a/src/HOL/Tools/function_package/fundef_package.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML Tue Mar 03 18:33:21 2009 +0100
@@ -99,8 +99,8 @@
val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
val ((fixes0, spec0), ctxt') =
prep (constrn_fxs fixspec) (map (single o apsnd single) eqnss) lthy
- val fixes = map (apfst (apfst Binding.base_name)) fixes0;
- val spec = map (apfst (apfst Binding.base_name)) spec0;
+ val fixes = map (apfst (apfst Binding.name_of)) fixes0;
+ val spec = map (apfst (apfst Binding.name_of)) spec0;
val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
val defname = mk_defname fixes
--- a/src/HOL/Tools/inductive_package.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML Tue Mar 03 18:33:21 2009 +0100
@@ -260,7 +260,7 @@
fun check_rule ctxt cs params ((binding, att), rule) =
let
- val err_name = Binding.display binding;
+ val err_name = Binding.str_of binding;
val params' = Term.variant_frees rule (Logic.strip_params rule);
val frees = rev (map Free params');
val concl = subst_bounds (frees, Logic.strip_assums_concl rule);
@@ -639,7 +639,7 @@
val rec_name =
if Binding.is_empty alt_name then
- Binding.name (space_implode "_" (map (Binding.base_name o fst) cnames_syn))
+ Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn))
else alt_name;
val ((rec_const, (_, fp_def)), ctxt') = ctxt |>
@@ -674,9 +674,9 @@
fun declare_rules kind rec_binding coind no_ind cnames intrs intr_bindings intr_atts
elims raw_induct ctxt =
let
- val rec_name = Binding.base_name rec_binding;
- val rec_qualified = Binding.qualify rec_name;
- val intr_names = map Binding.base_name intr_bindings;
+ val rec_name = Binding.name_of rec_binding;
+ val rec_qualified = Binding.qualify false rec_name;
+ val intr_names = map Binding.name_of intr_bindings;
val ind_case_names = RuleCases.case_names intr_names;
val induct =
if coind then
@@ -734,7 +734,7 @@
cs intros monos params cnames_syn ctxt =
let
val _ = null cnames_syn andalso error "No inductive predicates given";
- val names = map (Binding.base_name o fst) cnames_syn;
+ val names = map (Binding.name_of o fst) cnames_syn;
val _ = message (quiet_mode andalso not verbose)
("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^ commas_quote names);
@@ -749,7 +749,7 @@
val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs)
params intr_ts rec_preds_defs ctxt1;
val elims = if no_elim then [] else
- prove_elims quiet_mode cs params intr_ts (map Binding.base_name intr_names)
+ prove_elims quiet_mode cs params intr_ts (map Binding.name_of intr_names)
unfold rec_preds_defs ctxt1;
val raw_induct = zero_var_indexes
(if no_ind then Drule.asm_rl else
@@ -793,7 +793,7 @@
(* abbrevs *)
- val (_, ctxt1) = Variable.add_fixes (map (Binding.base_name o fst o fst) cnames_syn) lthy;
+ val (_, ctxt1) = Variable.add_fixes (map (Binding.name_of o fst o fst) cnames_syn) lthy;
fun get_abbrev ((name, atts), t) =
if can (Logic.strip_assums_concl #> Logic.dest_equals) t then
@@ -802,7 +802,7 @@
error "Abbreviations may not have names or attributes";
val ((x, T), rhs) = LocalDefs.abs_def (snd (LocalDefs.cert_def ctxt1 t));
val var =
- (case find_first (fn ((c, _), _) => Binding.base_name c = x) cnames_syn of
+ (case find_first (fn ((c, _), _) => Binding.name_of c = x) cnames_syn of
NONE => error ("Undeclared head of abbreviation " ^ quote x)
| SOME ((b, T'), mx) =>
if T <> T' then error ("Bad type specification for abbreviation " ^ quote x)
@@ -811,17 +811,17 @@
else NONE;
val abbrevs = map_filter get_abbrev spec;
- val bs = map (Binding.base_name o fst o fst) abbrevs;
+ val bs = map (Binding.name_of o fst o fst) abbrevs;
(* predicates *)
val pre_intros = filter_out (is_some o get_abbrev) spec;
- val cnames_syn' = filter_out (member (op =) bs o Binding.base_name o fst o fst) cnames_syn;
- val cs = map (Free o apfst Binding.base_name o fst) cnames_syn';
+ val cnames_syn' = filter_out (member (op =) bs o Binding.name_of o fst o fst) cnames_syn;
+ val cs = map (Free o apfst Binding.name_of o fst) cnames_syn';
val ps = map Free pnames;
- val (_, ctxt2) = lthy |> Variable.add_fixes (map (Binding.base_name o fst o fst) cnames_syn');
+ val (_, ctxt2) = lthy |> Variable.add_fixes (map (Binding.name_of o fst o fst) cnames_syn');
val _ = map (fn abbr => LocalDefs.fixed_abbrev abbr ctxt2) abbrevs;
val ctxt3 = ctxt2 |> fold (snd oo LocalDefs.fixed_abbrev) abbrevs;
val expand = Assumption.export_term ctxt3 lthy #> ProofContext.cert_term lthy;
@@ -854,7 +854,7 @@
in
lthy
|> LocalTheory.set_group (serial_string ())
- |> gen_add_inductive_i mk_def flags cs (map (apfst Binding.base_name o fst) ps) intrs monos
+ |> gen_add_inductive_i mk_def flags cs (map (apfst Binding.name_of o fst) ps) intrs monos
end;
val add_inductive_i = gen_add_inductive_i add_ind_def;
@@ -954,7 +954,7 @@
else if Binding.is_empty b then ((a, atts), B)
else error "Illegal nested case names"
| ((b, _), _) => error "Illegal simultaneous specification")
- | (a, _) => error ("Illegal local specification parameters for " ^ quote (Binding.base_name a)));
+ | (a, _) => error ("Illegal local specification parameters for " ^ quote (Binding.str_of a)));
fun gen_ind_decl mk_def coind =
P.fixes -- P.for_fixes --
--- a/src/HOL/Tools/inductive_set_package.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/HOL/Tools/inductive_set_package.ML Tue Mar 03 18:33:21 2009 +0100
@@ -464,7 +464,7 @@
| NONE => u)) |>
Pattern.rewrite_term thy [] [to_pred_proc thy eqns'] |>
eta_contract (member op = cs' orf is_pred pred_arities))) intros;
- val cnames_syn' = map (fn (b, _) => (Binding.map_base (suffix "p") b, NoSyn)) cnames_syn;
+ val cnames_syn' = map (fn (b, _) => (Binding.map_name (suffix "p") b, NoSyn)) cnames_syn;
val monos' = map (to_pred [] (Context.Proof ctxt)) monos;
val ({preds, intrs, elims, raw_induct, ...}, ctxt1) =
InductivePackage.add_ind_def
@@ -501,7 +501,7 @@
(* convert theorems to set notation *)
val rec_name =
if Binding.is_empty alt_name then
- Binding.name (space_implode "_" (map (Binding.base_name o fst) cnames_syn))
+ Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn))
else alt_name;
val cnames = map (LocalTheory.full_name ctxt3 o #1) cnames_syn; (* FIXME *)
val (intr_names, intr_atts) = split_list (map fst intros);
--- a/src/HOL/Tools/primrec_package.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/HOL/Tools/primrec_package.ML Tue Mar 03 18:33:21 2009 +0100
@@ -194,7 +194,7 @@
val def_name = Thm.def_name (Sign.base_name fname);
val rhs = singleton (Syntax.check_terms ctxt) raw_rhs;
val SOME var = get_first (fn ((b, _), mx) =>
- if Binding.base_name b = fname then SOME (b, mx) else NONE) fixes;
+ if Binding.name_of b = fname then SOME (b, mx) else NONE) fixes;
in (var, ((Binding.name def_name, []), rhs)) end;
@@ -231,7 +231,7 @@
let
val (fixes, spec) = prepare_spec prep_spec lthy raw_fixes raw_spec;
val eqns = fold_rev (process_eqn (fn v => Variable.is_fixed lthy v
- orelse exists (fn ((w, _), _) => v = Binding.base_name w) fixes) o snd) spec [];
+ orelse exists (fn ((w, _), _) => v = Binding.name_of w) fixes) o snd) spec [];
val tnames = distinct (op =) (map (#1 o snd) eqns);
val dts = find_dts (DatatypePackage.get_datatypes (ProofContext.theory_of lthy)) tnames tnames;
val main_fns = map (fn (tname, {index, ...}) =>
@@ -248,7 +248,7 @@
else primrec_error ("functions " ^ commas_quote names2 ^
"\nare not mutually recursive");
val prefix = space_implode "_" (map (Sign.base_name o #1) defs);
- val qualify = Binding.qualify prefix;
+ val qualify = Binding.qualify false prefix;
val spec' = (map o apfst)
(fn (b, attrs) => (qualify b, Code.add_default_eqn_attrib :: attrs)) spec;
val simp_atts = map (Attrib.internal o K)
@@ -299,7 +299,7 @@
P.name >> pair false) --| P.$$$ ")")) (false, "");
val old_primrec_decl =
- opt_unchecked_name -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop);
+ opt_unchecked_name -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop);
fun pipe_error t = P.!!! (Scan.fail_with (K
(cat_lines ["Equations must be separated by " ^ quote "|", quote t])));
--- a/src/HOL/Tools/recdef_package.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/HOL/Tools/recdef_package.ML Tue Mar 03 18:33:21 2009 +0100
@@ -320,7 +320,7 @@
val _ =
OuterSyntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)"
K.thy_goal
- ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.xname --
+ ((SpecParse.opt_thm_name ":" >> apfst Binding.name_of) -- P.xname --
Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
>> (fn ((thm_name, name), i) => recdef_tc thm_name name i));
--- a/src/HOL/Tools/specification_package.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/HOL/Tools/specification_package.ML Tue Mar 03 18:33:21 2009 +0100
@@ -232,7 +232,7 @@
val specification_decl =
P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop)
+ Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop)
val _ =
OuterSyntax.command "specification" "define constants by specification" K.thy_goal
@@ -243,7 +243,7 @@
val ax_specification_decl =
P.name --
(P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop))
+ Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop))
val _ =
OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal
--- a/src/HOLCF/Tools/fixrec_package.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/HOLCF/Tools/fixrec_package.ML Tue Mar 03 18:33:21 2009 +0100
@@ -16,7 +16,7 @@
-> (Attrib.binding * term) list -> local_theory -> local_theory
val add_fixpat: Attrib.binding * string list -> theory -> theory
- val add_fixpat_i: (binding * attribute list) * term list -> theory -> theory
+ val add_fixpat_i: Thm.binding * term list -> theory -> theory
val add_matchers: (string * string) list -> theory -> theory
val setup: theory -> theory
end;
@@ -175,7 +175,7 @@
(spec : (Attrib.binding * term) list)
(lthy : local_theory) =
let
- val names = map (Binding.base_name o fst o fst) fixes;
+ val names = map (Binding.name_of o fst o fst) fixes;
val all_names = space_implode "_" names;
val (lhss,rhss) = ListPair.unzip (map (dest_eqs o snd) spec);
val fixpoint = mk_fix (lambda_ctuple lhss (mk_ctuple rhss));
--- a/src/Pure/General/binding.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/General/binding.ML Tue Mar 03 18:33:21 2009 +0100
@@ -1,98 +1,99 @@
(* Title: Pure/General/binding.ML
Author: Florian Haftmann, TU Muenchen
+ Author: Makarius
Structured name bindings.
*)
-signature BASIC_BINDING =
-sig
- type binding
- val long_names: bool ref
- val short_names: bool ref
- val unique_names: bool ref
-end;
+type bstring = string; (*primitive names to be bound*)
signature BINDING =
sig
- include BASIC_BINDING
- val name_pos: string * Position.T -> binding
- val name: string -> binding
+ type binding
+ val dest: binding -> (string * bool) list * (string * bool) list * bstring
+ val str_of: binding -> string
+ val make: bstring * Position.T -> binding
+ val name: bstring -> binding
+ val pos_of: binding -> Position.T
+ val name_of: binding -> string
+ val map_name: (bstring -> bstring) -> binding -> binding
val empty: binding
- val map_base: (string -> string) -> binding -> binding
- val qualify: string -> binding -> binding
+ val is_empty: binding -> bool
+ val qualify: bool -> string -> binding -> binding
+ val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
val add_prefix: bool -> string -> binding -> binding
- val map_prefix: ((string * bool) list -> binding -> binding) -> binding -> binding
- val is_empty: binding -> bool
- val base_name: binding -> string
- val pos_of: binding -> Position.T
- val dest: binding -> (string * bool) list * string
- val separator: string
- val is_qualified: string -> bool
- val display: binding -> string
end;
-structure Binding : BINDING =
+structure Binding: BINDING =
struct
-(** global flags **)
+(** representation **)
-val long_names = ref false;
-val short_names = ref false;
-val unique_names = ref true;
+(* datatype *)
+type component = string * bool; (*name with mandatory flag*)
-(** qualification **)
-
-val separator = ".";
-val is_qualified = exists_string (fn s => s = separator);
+datatype binding = Binding of
+ {prefix: component list, (*system prefix*)
+ qualifier: component list, (*user qualifier*)
+ name: bstring, (*base name*)
+ pos: Position.T}; (*source position*)
-fun reject_qualified kind s =
- if is_qualified s then
- error ("Attempt to declare qualified " ^ kind ^ " " ^ quote s)
- else s;
+fun make_binding (prefix, qualifier, name, pos) =
+ Binding {prefix = prefix, qualifier = qualifier, name = name, pos = pos};
+
+fun map_binding f (Binding {prefix, qualifier, name, pos}) =
+ make_binding (f (prefix, qualifier, name, pos));
+
+fun dest (Binding {prefix, qualifier, name, ...}) = (prefix, qualifier, name);
-(** binding representation **)
+(* diagnostic output *)
-datatype binding = Binding of ((string * bool) list * string) * Position.T;
- (* (prefix components (with mandatory flag), base name, position) *)
-
-fun name_pos (name, pos) = Binding (([], name), pos);
-fun name name = name_pos (name, Position.none);
-val empty = name "";
+val str_of_components = implode o map (fn (s, true) => s ^ "!" | (s, false) => s ^ "?");
-fun map_binding f (Binding (prefix_name, pos)) = Binding (f prefix_name, pos);
-
-val map_base = map_binding o apsnd;
+fun str_of (Binding {prefix, qualifier, name, pos}) =
+ let
+ val text =
+ (if null prefix then "" else enclose "(" ")" (str_of_components prefix)) ^
+ str_of_components qualifier ^ ":" ^ name;
+ val props = Position.properties_of pos;
+ in Markup.markup (Markup.properties props (Markup.binding name)) text end;
-fun qualify_base path name =
- if path = "" orelse name = "" then name
- else path ^ separator ^ name;
+
+
+(** basic operations **)
-val qualify = map_base o qualify_base;
- (*FIXME should all operations on bare names move here from name_space.ML ?*)
+(* name and position *)
+
+fun make (name, pos) = make_binding ([], [], name, pos);
+fun name name = make (name, Position.none);
-fun add_prefix sticky "" b = b
- | add_prefix sticky prfx b = (map_binding o apfst)
- (cons ((*reject_qualified "prefix"*) prfx, sticky)) b;
+fun pos_of (Binding {pos, ...}) = pos;
+fun name_of (Binding {name, ...}) = name;
+
+fun map_name f = map_binding (fn (prefix, qualifier, name, pos) => (prefix, qualifier, f name, pos));
-fun map_prefix f (Binding ((prefix, name), pos)) =
- f prefix (name_pos (name, pos));
+val empty = name "";
+fun is_empty b = name_of b = "";
+
+
+(* user qualifier *)
-fun is_empty (Binding ((_, name), _)) = name = "";
-fun base_name (Binding ((_, name), _)) = name;
-fun pos_of (Binding (_, pos)) = pos;
-fun dest (Binding (prefix_name, _)) = prefix_name;
+fun qualify _ "" = I
+ | qualify mandatory qual = map_binding (fn (prefix, qualifier, name, pos) =>
+ (prefix, (qual, mandatory) :: qualifier, name, pos));
+
-fun display (Binding ((prefix, name), _)) =
- let
- fun mk_prefix (prfx, true) = prfx
- | mk_prefix (prfx, false) = enclose "(" ")" prfx
- in if not (! long_names) orelse null prefix orelse name = "" then name
- else space_implode "." (map mk_prefix prefix) ^ ":" ^ name
- end;
+(* system prefix *)
+
+fun map_prefix f = map_binding (fn (prefix, qualifier, name, pos) =>
+ (f prefix, qualifier, name, pos));
+
+fun add_prefix _ "" = I
+ | add_prefix mandatory prfx = map_prefix (cons (prfx, mandatory));
end;
-structure Basic_Binding : BASIC_BINDING = Binding;
-open Basic_Binding;
+type binding = Binding.binding;
+
--- a/src/Pure/General/markup.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/General/markup.ML Tue Mar 03 18:33:21 2009 +0100
@@ -12,9 +12,9 @@
val properties: (string * string) list -> T -> T
val nameN: string
val name: string -> T -> T
+ val bindingN: string val binding: string -> T
val groupN: string
val theory_nameN: string
- val idN: string
val kindN: string
val internalK: string
val property_internal: Properties.property
@@ -25,6 +25,7 @@
val end_columnN: string
val end_offsetN: string
val fileN: string
+ val idN: string
val position_properties': string list
val position_properties: string list
val positionN: string val position: T
@@ -107,6 +108,8 @@
structure Markup: MARKUP =
struct
+(** markup elements **)
+
(* basic markup *)
type T = string * Properties.T;
@@ -130,6 +133,8 @@
val nameN = "name";
fun name a = properties [(nameN, a)];
+val (bindingN, binding) = markup_string "binding" nameN;
+
val groupN = "group";
val theory_nameN = "theory_name";
@@ -278,7 +283,7 @@
-(* print mode operations *)
+(** print mode operations **)
val no_output = ("", "");
fun default_output (_: T) = no_output;
--- a/src/Pure/General/name_space.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/General/name_space.ML Tue Mar 03 18:33:21 2009 +0100
@@ -6,12 +6,18 @@
Cf. Pure/General/binding.ML
*)
-type bstring = string; (*simple names to be bound -- legacy*)
type xstring = string; (*external names*)
+signature BASIC_NAME_SPACE =
+sig
+ val long_names: bool ref
+ val short_names: bool ref
+ val unique_names: bool ref
+end;
+
signature NAME_SPACE =
sig
- include BASIC_BINDING
+ include BASIC_NAME_SPACE
val hidden: string -> string
val is_hidden: string -> bool
val separator: string (*single char*)
@@ -27,8 +33,9 @@
val empty: T
val intern: T -> xstring -> string
val extern: T -> string -> xstring
+ val extern_flags: {long_names: bool, short_names: bool, unique_names: bool} ->
+ T -> string -> xstring
val hide: bool -> string -> T -> T
- val get_accesses: T -> string -> xstring list
val merge: T * T -> T
type naming
val default_naming: naming
@@ -54,16 +61,13 @@
structure NameSpace: NAME_SPACE =
struct
-open Basic_Binding;
-
-
(** long identifiers **)
fun hidden name = "??." ^ name;
val is_hidden = String.isPrefix "??.";
-val separator = Binding.separator;
-val is_qualified = Binding.is_qualified;
+val separator = ".";
+val is_qualified = exists_string (fn s => s = separator);
val implode_name = space_implode separator;
val explode_name = space_explode separator;
@@ -133,19 +137,10 @@
| SOME ((name :: _, _), _) => (name, false)
| SOME (([], name' :: _), _) => (hidden name', true));
-fun ex_mapsto_in (NameSpace (tab, _)) name xname =
- (case Symtab.lookup tab xname of
- SOME ((name'::_, _), _) => name' = name
- | _ => false);
-
-fun get_accesses' valid_only (ns as (NameSpace (_, tab))) name =
+fun get_accesses (NameSpace (_, tab)) name =
(case Symtab.lookup tab name of
NONE => [name]
- | SOME (xnames, _) => if valid_only
- then filter (ex_mapsto_in ns name) xnames
- else xnames);
-
-val get_accesses = get_accesses' true;
+ | SOME (xnames, _) => xnames);
fun put_accesses name xnames (NameSpace (tab, xtab)) =
NameSpace (tab, Symtab.update (name, (xnames, stamp ())) xtab);
@@ -158,20 +153,30 @@
fun intern space xname = #1 (lookup space xname);
-fun extern space name =
+fun extern_flags {long_names, short_names, unique_names} space name =
let
fun valid unique xname =
let val (name', uniq) = lookup space xname
in name = name' andalso (uniq orelse not unique) end;
fun ext [] = if valid false name then name else hidden name
- | ext (nm :: nms) = if valid (! unique_names) nm then nm else ext nms;
+ | ext (nm :: nms) = if valid unique_names nm then nm else ext nms;
in
- if ! long_names then name
- else if ! short_names then base name
- else ext (get_accesses' false space name)
+ if long_names then name
+ else if short_names then base name
+ else ext (get_accesses space name)
end;
+val long_names = ref false;
+val short_names = ref false;
+val unique_names = ref true;
+
+fun extern space name =
+ extern_flags
+ {long_names = ! long_names,
+ short_names = ! short_names,
+ unique_names = ! unique_names} space name;
+
(* basic operations *)
@@ -203,7 +208,7 @@
space
|> add_name' name name
|> fold (del_name name) (if fully then names else names inter_string [base name])
- |> fold (del_name_extra name) (get_accesses' false space name)
+ |> fold (del_name_extra name) (get_accesses space name)
end;
@@ -289,13 +294,13 @@
in space |> fold (add_name name) accs |> put_accesses name accs' end;
fun full_name naming b =
- let val (prefix, bname) = Binding.dest b
- in full_internal (apply_prefix prefix naming) bname end;
+ let val (prefix, qualifier, bname) = Binding.dest b
+ in full_internal (apply_prefix (prefix @ qualifier) naming) bname end;
fun declare bnaming b =
let
- val (prefix, bname) = Binding.dest b;
- val naming = apply_prefix prefix bnaming;
+ val (prefix, qualifier, bname) = Binding.dest b;
+ val naming = apply_prefix (prefix @ qualifier) bnaming;
val name = full_internal naming bname;
in declare_internal naming name #> pair name end;
@@ -331,3 +336,7 @@
val explode = explode_name;
end;
+
+structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace;
+open BasicNameSpace;
+
--- a/src/Pure/Isar/args.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Isar/args.ML Tue Mar 03 18:33:21 2009 +0100
@@ -170,7 +170,7 @@
val name_source_position = named >> T.source_position_of;
val name = named >> T.content_of;
-val binding = P.position name >> Binding.name_pos;
+val binding = P.position name >> Binding.make;
val alt_name = alt_string >> T.content_of;
val symbol = symbolic >> T.content_of;
val liberal_name = symbol || name;
--- a/src/Pure/Isar/attrib.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Isar/attrib.ML Tue Mar 03 18:33:21 2009 +0100
@@ -118,8 +118,7 @@
fun attribute thy = attribute_i thy o intern_src thy;
fun eval_thms ctxt args = ProofContext.note_thmss Thm.theoremK
- [((Binding.empty, []),
- map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
+ [(Thm.empty_binding, map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
|> fst |> maps snd;
--- a/src/Pure/Isar/class.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Isar/class.ML Tue Mar 03 18:33:21 2009 +0100
@@ -201,7 +201,7 @@
| check_element e = [()];
val _ = map check_element syntax_elems;
fun fork_syn (Element.Fixes xs) =
- fold_map (fn (c, ty, syn) => cons (Binding.base_name c, syn) #> pair (c, ty, NoSyn)) xs
+ fold_map (fn (c, ty, syn) => cons (Binding.name_of c, syn) #> pair (c, ty, NoSyn)) xs
#>> Element.Fixes
| fork_syn x = pair x;
val (elems, global_syntax) = fold_map fork_syn syntax_elems [];
@@ -228,7 +228,7 @@
val raw_params = (snd o chop (length supparams)) all_params;
fun add_const (b, SOME raw_ty, _) thy =
let
- val v = Binding.base_name b;
+ val v = Binding.name_of b;
val c = Sign.full_bname thy v;
val ty = map_atyps (K (TFree (Name.aT, base_sort))) raw_ty;
val ty0 = Type.strip_sorts ty;
@@ -265,8 +265,7 @@
|> add_consts bname class base_sort sups supparams global_syntax
|-> (fn (param_map, params) => AxClass.define_class (bname, supsort)
(map (fst o snd) params)
- [((Binding.empty, []),
- Option.map (globalize param_map) raw_pred |> the_list)]
+ [(Thm.empty_binding, Option.map (globalize param_map) raw_pred |> the_list)]
#> snd
#> `get_axiom
#-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params
--- a/src/Pure/Isar/constdefs.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Isar/constdefs.ML Tue Mar 03 18:33:21 2009 +0100
@@ -9,11 +9,9 @@
signature CONSTDEFS =
sig
val add_constdefs: (binding * string option) list *
- ((binding * string option * mixfix) option *
- (Attrib.binding * string)) list -> theory -> theory
+ ((binding * string option * mixfix) option * (Attrib.binding * string)) list -> theory -> theory
val add_constdefs_i: (binding * typ option) list *
- ((binding * typ option * mixfix) option *
- ((binding * attribute list) * term)) list -> theory -> theory
+ ((binding * typ option * mixfix) option * (Thm.binding * term)) list -> theory -> theory
end;
structure Constdefs: CONSTDEFS =
@@ -38,7 +36,7 @@
val prop = prep_prop var_ctxt raw_prop;
val (c, T) = #1 (LocalDefs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
val _ =
- (case Option.map Binding.base_name d of
+ (case Option.map Binding.name_of d of
NONE => ()
| SOME c' =>
if c <> c' then
@@ -46,7 +44,7 @@
else ());
val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_bname thy c, T))] prop;
- val name = Thm.def_name_optional c (Binding.base_name raw_name);
+ val name = Thm.def_name_optional c (Binding.name_of raw_name);
val atts = map (prep_att thy) raw_atts;
val thy' =
--- a/src/Pure/Isar/element.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Isar/element.ML Tue Mar 03 18:33:21 2009 +0100
@@ -96,7 +96,7 @@
fun map_ctxt {binding, typ, term, pattern, fact, attrib} =
fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) => (binding x, Option.map typ T, mx)))
| Constrains xs => Constrains (xs |> map (fn (x, T) =>
- (Binding.base_name (binding (Binding.name x)), typ T)))
+ (Binding.name_of (binding (Binding.name x)), typ T)))
| Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map pattern ps)))))
| Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
@@ -125,11 +125,9 @@
map (fn y => Pretty.block [Pretty.str " ", Pretty.keyword sep, Pretty.brk 1, y]) ys;
fun pretty_name_atts ctxt (b, atts) sep =
- let val name = Binding.display b in
- if name = "" andalso null atts then []
- else [Pretty.block
- (Pretty.breaks (Pretty.str name :: Attrib.pretty_attribs ctxt atts @ [Pretty.str sep]))]
- end;
+ if Binding.is_empty b andalso null atts then []
+ else [Pretty.block (Pretty.breaks
+ (Pretty.str (Binding.str_of b) :: Attrib.pretty_attribs ctxt atts @ [Pretty.str sep]))];
(* pretty_stmt *)
@@ -145,8 +143,8 @@
Pretty.block (Pretty.breaks (prt_name_atts a ":" @ prt_terms (map fst ts)));
fun prt_var (x, SOME T) = Pretty.block
- [Pretty.str (Binding.base_name x ^ " ::"), Pretty.brk 1, prt_typ T]
- | prt_var (x, NONE) = Pretty.str (Binding.base_name x);
+ [Pretty.str (Binding.name_of x ^ " ::"), Pretty.brk 1, prt_typ T]
+ | prt_var (x, NONE) = Pretty.str (Binding.name_of x);
val prt_vars = separate (Pretty.keyword "and") o map prt_var;
fun prt_obtain (_, ([], ts)) = Pretty.block (Pretty.breaks (prt_terms ts))
@@ -170,9 +168,9 @@
fun prt_mixfix NoSyn = []
| prt_mixfix mx = [Pretty.brk 2, Syntax.pretty_mixfix mx];
- fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (Binding.base_name x ^ " ::") ::
+ fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (Binding.name_of x ^ " ::") ::
Pretty.brk 1 :: prt_typ T :: Pretty.brk 1 :: prt_mixfix mx)
- | prt_fix (x, NONE, mx) = Pretty.block (Pretty.str (Binding.base_name x) ::
+ | prt_fix (x, NONE, mx) = Pretty.block (Pretty.str (Binding.name_of x) ::
Pretty.brk 1 :: prt_mixfix mx);
fun prt_constrain (x, T) = prt_fix (Binding.name x, SOME T, NoSyn);
@@ -296,7 +294,7 @@
gen_witness_proof (fn after_qed' => fn propss =>
Proof.map_context (K goal_ctxt)
#> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
- cmd NONE after_qed' (map (pair (Binding.empty, [])) propss))
+ cmd NONE after_qed' (map (pair Thm.empty_binding) propss))
(fn wits => fn _ => after_qed wits) wit_propss [];
end;
@@ -504,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_base (Thm.def_name_optional c) name, atts), [(t', ps)])) end);
+ in (t', ((Binding.map_name (Thm.def_name_optional 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);
@@ -529,7 +527,7 @@
fun prep_facts prep_name get intern ctxt =
map_ctxt
- {binding = Binding.map_base prep_name,
+ {binding = Binding.map_name prep_name,
typ = I,
term = I,
pattern = I,
--- a/src/Pure/Isar/expression.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Isar/expression.ML Tue Mar 03 18:33:21 2009 +0100
@@ -88,17 +88,13 @@
if null dups then () else error (message ^ commas dups)
end;
- fun match_bind (n, b) = (n = Binding.base_name b);
+ fun match_bind (n, b) = (n = Binding.name_of b);
fun parm_eq ((b1, mx1: mixfix), (b2, mx2)) =
(* FIXME: cannot compare bindings for equality, instead check for equal name and syntax *)
- (Binding.base_name b1 = Binding.base_name b2) andalso
- (if mx1 = mx2 then true
- else error ("Conflicting syntax for parameter" ^ quote (Binding.display b1) ^
- " in expression."));
+ Binding.name_of b1 = Binding.name_of b2 andalso
+ (mx1 = mx2 orelse
+ error ("Conflicting syntax for parameter " ^ quote (Binding.str_of b1) ^ " in expression"));
- fun bind_eq (b1, b2) = (Binding.base_name b1 = Binding.base_name b2);
- (* FIXME: cannot compare bindings for equality. *)
-
fun params_loc loc =
(Locale.params_of thy loc |> map (fn (p, _, mx) => (p, mx)), loc);
fun params_inst (expr as (loc, (prfx, Positional insts))) =
@@ -133,8 +129,8 @@
val (implicit, expr') = params_expr expr;
- val implicit' = map (#1 #> Binding.base_name) implicit;
- val fixed' = map (#1 #> Binding.base_name) fixed;
+ val implicit' = map (#1 #> Binding.name_of) implicit;
+ val fixed' = map (#1 #> Binding.name_of) fixed;
val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
val implicit'' = if strict then []
else let val _ = reject_dups
@@ -310,14 +306,12 @@
(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_base (Thm.def_name_optional c) name, atts), (t', no_binds ps))
- end))
+ in ((Binding.map_name (Thm.def_name_optional c) name, atts), (t', no_binds ps)) end))
| e => e)
end;
fun finish_primitive parms _ (Fixes fixes) = Fixes (map (fn (binding, _, mx) =>
- let val x = Binding.base_name binding
+ let val x = Binding.name_of binding
in (binding, AList.lookup (op =) parms x, mx) end) fixes)
| finish_primitive _ _ (Constrains _) = Constrains []
| finish_primitive _ close (Assumes asms) = close (Assumes asms)
@@ -328,7 +322,7 @@
let
val thy = ProofContext.theory_of ctxt;
val (parm_names, parm_types) = Locale.params_of thy loc |>
- map_split (fn (b, SOME T, _) => (Binding.base_name b, T));
+ map_split (fn (b, SOME T, _) => (Binding.name_of b, T));
val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
in (loc, morph) end;
@@ -360,7 +354,7 @@
fun prep_insts (loc, (prfx, inst)) (i, insts, ctxt) =
let
val (parm_names, parm_types) = Locale.params_of thy loc |>
- map_split (fn (b, SOME T, _) => (Binding.base_name b, T))
+ map_split (fn (b, SOME T, _) => (Binding.name_of b, T))
(*FIXME return value of Locale.params_of has strange type*)
val inst' = prep_inst ctxt parm_names inst;
val parm_types' = map (TypeInfer.paramify_vars o
@@ -394,7 +388,7 @@
prep_concl raw_concl (insts', elems, ctxt5);
(* Retrieve parameter types *)
- val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Binding.base_name o #1) fixes)
+ val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Binding.name_of o #1) fixes)
| _ => fn ps => ps) (Fixes fors :: elems') [];
val (Ts, ctxt7) = fold_map ProofContext.inferred_param xs ctxt6;
val parms = xs ~~ Ts; (* params from expression and elements *)
--- a/src/Pure/Isar/isar_cmd.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Tue Mar 03 18:33:21 2009 +0100
@@ -161,7 +161,7 @@
(* axioms *)
fun add_axms f args thy =
- f (map (fn ((b, ax), srcs) => ((Binding.base_name b, ax), map (Attrib.attribute thy) srcs)) args) thy;
+ f (map (fn ((b, ax), srcs) => ((Binding.name_of b, ax), map (Attrib.attribute thy) srcs)) args) thy;
val add_axioms = add_axms (snd oo PureThy.add_axioms_cmd);
--- a/src/Pure/Isar/local_defs.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Isar/local_defs.ML Tue Mar 03 18:33:21 2009 +0100
@@ -11,8 +11,8 @@
val mk_def: Proof.context -> (string * term) list -> term list
val expand: cterm list -> thm -> thm
val def_export: Assumption.export
- val add_defs: ((binding * mixfix) * ((binding * attribute list) * term)) list ->
- Proof.context -> (term * (string * thm)) list * Proof.context
+ val add_defs: ((binding * mixfix) * (Thm.binding * term)) list -> Proof.context ->
+ (term * (string * thm)) list * Proof.context
val add_def: (binding * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
val fixed_abbrev: (binding * mixfix) * term -> Proof.context ->
(term * term) * Proof.context
@@ -90,8 +90,8 @@
let
val ((bvars, mxs), specs) = defs |> split_list |>> split_list;
val ((bfacts, atts), rhss) = specs |> split_list |>> split_list;
- val xs = map Binding.base_name bvars;
- val names = map2 (Binding.map_base o Thm.def_name_optional) xs bfacts;
+ val xs = map Binding.name_of bvars;
+ val names = map2 (Binding.map_name o Thm.def_name_optional) xs bfacts;
val eqs = mk_def ctxt (xs ~~ rhss);
val lhss = map (fst o Logic.dest_equals) eqs;
in
@@ -104,7 +104,7 @@
end;
fun add_def (var, rhs) ctxt =
- let val ([(lhs, (_, th))], ctxt') = add_defs [(var, ((Binding.empty, []), rhs))] ctxt
+ let val ([(lhs, (_, th))], ctxt') = add_defs [(var, (Thm.empty_binding, rhs))] ctxt
in ((lhs, th), ctxt') end;
--- a/src/Pure/Isar/locale.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Isar/locale.ML Tue Mar 03 18:33:21 2009 +0100
@@ -194,7 +194,7 @@
fun axioms_of thy = #axioms o the_locale thy;
fun instance_of thy name morph = params_of thy name |>
- map ((fn (b, T, _) => Free (Binding.base_name b, the T)) #> Morphism.term morph);
+ map ((fn (b, T, _) => Free (Binding.name_of b, the T)) #> Morphism.term morph);
fun specification_of thy = #spec o the_locale thy;
@@ -464,8 +464,7 @@
fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi));
fun add_decls add loc decl =
- ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, stamp ())))
- #>
+ ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, stamp ()))) #>
add_thmss loc Thm.internalK
[((Binding.empty, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
--- a/src/Pure/Isar/obtain.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Isar/obtain.ML Tue Mar 03 18:33:21 2009 +0100
@@ -40,11 +40,9 @@
sig
val thatN: string
val obtain: string -> (binding * string option * mixfix) list ->
- (Attrib.binding * (string * string list) list) list ->
- bool -> Proof.state -> Proof.state
+ (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
val obtain_i: string -> (binding * typ option * mixfix) list ->
- ((binding * attribute list) * (term * term list) list) list ->
- bool -> Proof.state -> Proof.state
+ (Thm.binding * (term * term list) list) list -> bool -> Proof.state -> Proof.state
val result: (Proof.context -> tactic) -> thm list -> Proof.context ->
(cterm list * thm list) * Proof.context
val guess: (binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
@@ -121,7 +119,7 @@
(*obtain vars*)
val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
- val xs = map (Binding.base_name o #1) vars;
+ val xs = map (Binding.name_of o #1) vars;
(*obtain asms*)
val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
@@ -155,14 +153,14 @@
in
state
|> Proof.enter_forward
- |> Proof.have_i NONE (K I) [((Binding.empty, []), [(obtain_prop, [])])] int
+ |> Proof.have_i NONE (K I) [(Thm.empty_binding, [(obtain_prop, [])])] int
|> Proof.proof (SOME Method.succeed_text) |> Seq.hd
|> Proof.fix_i [(Binding.name thesisN, NONE, NoSyn)]
|> Proof.assume_i
[((Binding.name that_name, [ContextRules.intro_query NONE]), [(that_prop, [])])]
|> `Proof.the_facts
||> Proof.chain_facts chain_facts
- ||> Proof.show_i NONE after_qed [((Binding.empty, []), [(thesis, [])])] false
+ ||> Proof.show_i NONE after_qed [(Thm.empty_binding, [(thesis, [])])] false
|-> Proof.refine_insert
end;
@@ -260,7 +258,7 @@
fun inferred_type (binding, _, mx) ctxt =
let
- val x = Binding.base_name binding;
+ val x = Binding.name_of binding;
val (T, ctxt') = ProofContext.inferred_param x ctxt
in ((x, T, mx), ctxt') end;
@@ -295,7 +293,7 @@
|> Proof.map_context (K ctxt')
|> Proof.fix_i (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms)
|> `Proof.context_of |-> (fn fix_ctxt => Proof.assm_i
- (obtain_export fix_ctxt rule (map cert ts)) [((Binding.empty, []), asms)])
+ (obtain_export fix_ctxt rule (map cert ts)) [(Thm.empty_binding, asms)])
|> Proof.add_binds_i AutoBind.no_facts
end;
@@ -313,7 +311,7 @@
|> Proof.fix_i [(Binding.name AutoBind.thesisN, NONE, NoSyn)]
|> Proof.chain_facts chain_facts
|> Proof.local_goal print_result (K I) (apsnd (rpair I))
- "guess" before_qed after_qed [((Binding.empty, []), [Logic.mk_term goal, goal])]
+ "guess" before_qed after_qed [(Thm.empty_binding, [Logic.mk_term goal, goal])]
|> Proof.refine (Method.primitive_text (K (Goal.init (cert thesis)))) |> Seq.hd
end;
--- a/src/Pure/Isar/outer_parse.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Isar/outer_parse.ML Tue Mar 03 18:33:21 2009 +0100
@@ -228,7 +228,7 @@
(* names and text *)
val name = group "name declaration" (short_ident || sym_ident || string || number);
-val binding = position name >> Binding.name_pos;
+val binding = position name >> Binding.make;
val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number);
val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
val path = group "file name/path specification" name >> Path.explode;
--- a/src/Pure/Isar/proof.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Isar/proof.ML Tue Mar 03 18:33:21 2009 +0100
@@ -48,23 +48,18 @@
val assm: Assumption.export ->
(Attrib.binding * (string * string list) list) list -> state -> state
val assm_i: Assumption.export ->
- ((binding * attribute list) * (term * term list) list) list -> state -> state
+ (Thm.binding * (term * term list) list) list -> state -> state
val assume: (Attrib.binding * (string * string list) list) list -> state -> state
- val assume_i: ((binding * attribute list) * (term * term list) list) list ->
- state -> state
+ val assume_i: (Thm.binding * (term * term list) list) list -> state -> state
val presume: (Attrib.binding * (string * string list) list) list -> state -> state
- val presume_i: ((binding * attribute list) * (term * term list) list) list ->
- state -> state
- val def: (Attrib.binding * ((binding * mixfix) * (string * string list))) list ->
- state -> state
- val def_i: ((binding * attribute list) *
- ((binding * mixfix) * (term * term list))) list -> state -> state
+ val presume_i: (Thm.binding * (term * term list) list) list -> state -> state
+ val def: (Attrib.binding * ((binding * mixfix) * (string * string list))) list -> state -> state
+ val def_i: (Thm.binding * ((binding * mixfix) * (term * term list))) list -> state -> state
val chain: state -> state
val chain_facts: thm list -> state -> state
val get_thmss: state -> (Facts.ref * Attrib.src list) list -> thm list
val note_thmss: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
- val note_thmss_i: ((binding * attribute list) *
- (thm list * attribute list) list) list -> state -> state
+ val note_thmss_i: (Thm.binding * (thm list * attribute list) list) list -> state -> state
val from_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
val from_thmss_i: ((thm list * attribute list) list) list -> state -> state
val with_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
@@ -107,11 +102,11 @@
val have: Method.text option -> (thm list list -> state -> state) ->
(Attrib.binding * (string * string list) list) list -> bool -> state -> state
val have_i: Method.text option -> (thm list list -> state -> state) ->
- ((binding * attribute list) * (term * term list) list) list -> bool -> state -> state
+ (Thm.binding * (term * term list) list) list -> bool -> state -> state
val show: Method.text option -> (thm list list -> state -> state) ->
(Attrib.binding * (string * string list) list) list -> bool -> state -> state
val show_i: Method.text option -> (thm list list -> state -> state) ->
- ((binding * attribute list) * (term * term list) list) list -> bool -> state -> state
+ (Thm.binding * (term * term list) list) list -> bool -> state -> state
val schematic_goal: state -> bool
val is_relevant: state -> bool
val local_future_proof: (state -> ('a * state) Future.future) ->
--- a/src/Pure/Isar/proof_context.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML Tue Mar 03 18:33:21 2009 +0100
@@ -103,12 +103,10 @@
val sticky_prefix: string -> Proof.context -> Proof.context
val restore_naming: Proof.context -> Proof.context -> Proof.context
val reset_naming: Proof.context -> Proof.context
- val note_thmss: string ->
- ((binding * attribute list) * (Facts.ref * attribute list) list) list ->
- Proof.context -> (string * thm list) list * Proof.context
- val note_thmss_i: string ->
- ((binding * attribute list) * (thm list * attribute list) list) list ->
- Proof.context -> (string * thm list) list * Proof.context
+ val note_thmss: string -> (Thm.binding * (Facts.ref * attribute list) list) list ->
+ Proof.context -> (string * thm list) list * Proof.context
+ val note_thmss_i: string -> (Thm.binding * (thm list * attribute list) list) list ->
+ Proof.context -> (string * thm list) list * Proof.context
val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
val read_vars: (binding * string option * mixfix) list -> Proof.context ->
(binding * typ option * mixfix) list * Proof.context
@@ -121,10 +119,10 @@
val auto_fixes: Proof.context * (term list list * 'a) -> Proof.context * (term list list * 'a)
val bind_fixes: string list -> Proof.context -> (term -> term) * Proof.context
val add_assms: Assumption.export ->
- ((binding * attribute list) * (string * string list) list) list ->
+ (Thm.binding * (string * string list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
val add_assms_i: Assumption.export ->
- ((binding * attribute list) * (term * term list) list) list ->
+ (Thm.binding * (term * term list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
val add_cases: bool -> (string * RuleCases.T option) list -> Proof.context -> Proof.context
val apply_case: RuleCases.T -> Proof.context -> (string * term list) list * Proof.context
@@ -1010,7 +1008,7 @@
fun prep_vars prep_typ internal =
fold_map (fn (raw_b, raw_T, raw_mx) => fn ctxt =>
let
- val raw_x = Binding.base_name raw_b;
+ val raw_x = Binding.name_of raw_b;
val (x, mx) = Syntax.const_mixfix raw_x raw_mx;
val _ = Syntax.is_identifier (no_skolem internal x) orelse
error ("Illegal variable name: " ^ quote x);
@@ -1019,7 +1017,7 @@
if internal then T
else Type.no_tvars T handle TYPE (msg, _, _) => error msg;
val opt_T = Option.map (cond_tvars o cert_typ ctxt o prep_typ ctxt) raw_T;
- val var = (Binding.map_base (K x) raw_b, opt_T, mx);
+ val var = (Binding.map_name (K x) raw_b, opt_T, mx);
in (var, ctxt |> declare_var (x, opt_T, mx) |> #2) end);
in
@@ -1093,7 +1091,7 @@
fun add_abbrev mode tags (b, raw_t) ctxt =
let
val t0 = cert_term (ctxt |> set_mode mode_abbrev) raw_t
- handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.display b));
+ handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.str_of b));
val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0];
val ((lhs, rhs), consts') = consts_of ctxt
|> Consts.abbreviate (Syntax.pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode tags (b, t);
@@ -1120,7 +1118,7 @@
fun gen_fixes prep raw_vars ctxt =
let
val (vars, _) = prep raw_vars ctxt;
- val (xs', ctxt') = Variable.add_fixes (map (Binding.base_name o #1) vars) ctxt;
+ val (xs', ctxt') = Variable.add_fixes (map (Binding.name_of o #1) vars) ctxt;
val ctxt'' =
ctxt'
|> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
--- a/src/Pure/Isar/specification.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Isar/specification.ML Tue Mar 03 18:33:21 2009 +0100
@@ -140,7 +140,7 @@
fun gen_axioms do_print prep raw_vars raw_specs thy =
let
val ((vars, specs), _) = prep raw_vars [raw_specs] (ProofContext.init thy);
- val xs = map (fn ((b, T), _) => (Binding.base_name b, T)) vars;
+ val xs = map (fn ((b, T), _) => (Binding.name_of b, T)) vars;
(*consts*)
val (consts, consts_thy) = thy |> fold_map (Theory.specify_const []) vars;
@@ -148,8 +148,8 @@
(*axioms*)
val (axioms, axioms_thy) = consts_thy |> fold_map (fn ((b, atts), props) =>
- fold_map Thm.add_axiom
- ((map o apfst) Binding.name (PureThy.name_multi (Binding.base_name b) (map subst props)))
+ fold_map Thm.add_axiom (* FIXME proper use of binding!? *)
+ ((map o apfst) Binding.name (PureThy.name_multi (Binding.name_of b) (map subst props)))
#>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])]))) specs;
val (facts, thy') = axioms_thy |> PureThy.note_thmss Thm.axiomK
(Attrib.map_facts (Attrib.attribute_i axioms_thy) axioms);
@@ -169,19 +169,19 @@
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_base (Thm.def_name_optional x) raw_name;
+ val name = Binding.map_name (Thm.def_name_optional x) raw_name;
val var =
(case vars of
[] => (Binding.name x, NoSyn)
| [((b, _), mx)] =>
let
- val y = Binding.base_name b;
+ val y = Binding.name_of b;
val _ = x = y orelse
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
- (var, ((Binding.map_base (suffix "_raw") name, []), rhs));
+ (var, ((Binding.map_name (suffix "_raw") name, []), rhs));
val ((def_name, [th']), lthy3) = lthy2 |> LocalTheory.note Thm.definitionK
((name, Code.add_default_eqn_attrib :: atts), [prove lthy2 th]);
@@ -208,7 +208,7 @@
[] => (Binding.name x, NoSyn)
| [((b, _), mx)] =>
let
- val y = Binding.base_name b;
+ val y = Binding.name_of b;
val _ = x = y orelse
error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
Position.str_of (Binding.pos_of b));
@@ -269,11 +269,10 @@
| Element.Obtains obtains =>
let
val case_names = obtains |> map_index (fn (i, (b, _)) =>
- let val name = Binding.base_name b
- in if name = "" then string_of_int (i + 1) else name end);
+ if Binding.is_empty b then string_of_int (i + 1) else Binding.name_of b);
val constraints = obtains |> map (fn (_, (vars, _)) =>
Element.Constrains
- (vars |> map_filter (fn (x, SOME T) => SOME (Binding.base_name x, T) | _ => NONE)));
+ (vars |> map_filter (fn (x, SOME T) => SOME (Binding.name_of x, T) | _ => NONE)));
val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
@@ -283,7 +282,7 @@
fun assume_case ((name, (vars, _)), asms) ctxt' =
let
val bs = map fst vars;
- val xs = map Binding.base_name bs;
+ val xs = map Binding.name_of bs;
val props = map fst asms;
val (Ts, _) = ctxt'
|> fold Variable.declare_term props
--- a/src/Pure/Isar/theory_target.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML Tue Mar 03 18:33:21 2009 +0100
@@ -188,8 +188,8 @@
val arg = (b', Term.close_schematic_term rhs');
val similar_body = Type.similar_types (rhs, rhs');
(* FIXME workaround based on educated guess *)
- val (prefix', _) = Binding.dest b';
- val class_global = Binding.base_name b = Binding.base_name b'
+ val (prefix', _, _) = Binding.dest b';
+ val class_global = Binding.name_of b = Binding.name_of b'
andalso not (null prefix')
andalso (fst o snd o split_last) prefix' = Class_Target.class_prefix target;
in
@@ -206,14 +206,15 @@
Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
end;
+fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
+
fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy =
let
- val c = Binding.base_name b;
+ val c = Binding.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;
val (mx1, mx2, mx3) = fork_mixfix ta mx;
- fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
val declare_const =
(case Class_Target.instantiation_param lthy c of
SOME c' =>
@@ -241,7 +242,7 @@
fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((b, mx), t) lthy =
let
- val c = Binding.base_name b;
+ val c = Binding.name_of b;
val tags = LocalTheory.group_position_of lthy;
val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
val target_ctxt = LocalTheory.target_of lthy;
@@ -278,8 +279,8 @@
val thy = ProofContext.theory_of lthy;
val thy_ctxt = ProofContext.init thy;
- val c = Binding.base_name b;
- val name' = Binding.map_base (Thm.def_name_optional c) name;
+ val c = Binding.name_of b;
+ val name' = Binding.map_name (Thm.def_name_optional c) 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' [];
@@ -299,7 +300,7 @@
then (fn name => fn eq => Thm.add_def false false (Binding.name name, Logic.mk_equals eq))
else (fn name => fn (Const (c, _), rhs) => AxClass.define_overloaded name (c, rhs)));
val (global_def, lthy3) = lthy2
- |> LocalTheory.theory_result (define_const (Binding.base_name name') (lhs', rhs'));
+ |> LocalTheory.theory_result (define_const (Binding.name_of name') (lhs', rhs'));
val def = LocalDefs.trans_terms lthy3
[(*c == global.c xs*) local_def,
(*global.c xs == rhs'*) global_def,
--- a/src/Pure/Thy/thy_output.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML Tue Mar 03 18:33:21 2009 +0100
@@ -519,9 +519,9 @@
fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option;";
fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"
-fun output_ml ml src ctxt (txt, pos) =
+fun output_ml ml _ ctxt (txt, pos) =
(ML_Context.eval_in (SOME ctxt) false pos (ml txt);
- (if ! source then str_of_source src else SymbolPos.content (SymbolPos.explode (txt, pos)))
+ SymbolPos.content (SymbolPos.explode (txt, pos))
|> (if ! quotes then quote else I)
|> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
else
--- a/src/Pure/Tools/find_theorems.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Tools/find_theorems.ML Tue Mar 03 18:33:21 2009 +0100
@@ -306,14 +306,11 @@
fun nicer_shortest ctxt =
let
- val ns = ProofContext.theory_of ctxt
- |> PureThy.facts_of
- |> Facts.space_of;
+ (* FIXME global name space!? *)
+ val space = Facts.space_of (PureThy.facts_of (ProofContext.theory_of ctxt));
- val len_sort = sort (int_ord o (pairself size));
- fun shorten s = (case len_sort (NameSpace.get_accesses ns s) of
- [] => s
- | s'::_ => s');
+ val shorten =
+ NameSpace.extern_flags {long_names = false, short_names = false, unique_names = false} space;
fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
nicer_name (shorten x, i) (shorten y, j)
--- a/src/Pure/axclass.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/axclass.ML Tue Mar 03 18:33:21 2009 +0100
@@ -8,7 +8,7 @@
signature AX_CLASS =
sig
val define_class: bstring * class list -> string list ->
- ((binding * attribute list) * term list) list -> theory -> class * theory
+ (Thm.binding * term list) list -> theory -> class * theory
val add_classrel: thm -> theory -> theory
val add_arity: thm -> theory -> theory
val prove_classrel: class * class -> tactic -> theory -> theory
--- a/src/Pure/more_thm.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/more_thm.ML Tue Mar 03 18:33:21 2009 +0100
@@ -40,6 +40,8 @@
val close_derivation: thm -> thm
val add_axiom: binding * term -> theory -> thm * theory
val add_def: bool -> bool -> binding * term -> theory -> thm * theory
+ type binding = binding * attribute list
+ val empty_binding: binding
val rule_attribute: (Context.generic -> thm -> thm) -> attribute
val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute
val theory_attributes: attribute list -> theory * thm -> theory * thm
@@ -301,6 +303,9 @@
(** attributes **)
+type binding = binding * attribute list;
+val empty_binding: binding = (Binding.empty, []);
+
fun rule_attribute f (x, th) = (x, f x th);
fun declaration_attribute f (x, th) = (f th x, th);
--- a/src/Pure/pure_setup.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/pure_setup.ML Tue Mar 03 18:33:21 2009 +0100
@@ -33,7 +33,7 @@
map (fn (x, y) => Pretty.str (x ^ "=" ^ y)) o Position.properties_of));
install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm);
install_pp (make_pp ["Thm", "cterm"] ProofDisplay.pprint_cterm);
-install_pp (make_pp ["Binding", "binding"] (Pretty.pprint o Pretty.str o Binding.display));
+install_pp (make_pp ["Binding", "binding"] (Pretty.pprint o Pretty.str o Binding.str_of));
install_pp (make_pp ["Thm", "ctyp"] ProofDisplay.pprint_ctyp);
install_pp (make_pp ["Context", "theory"] Context.pprint_thy);
install_pp (make_pp ["Context", "theory_ref"] Context.pprint_thy_ref);
--- a/src/Pure/pure_thy.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/pure_thy.ML Tue Mar 03 18:33:21 2009 +0100
@@ -31,10 +31,10 @@
val add_thm: (binding * thm) * attribute list -> theory -> thm * theory
val add_thmss: ((binding * thm list) * attribute list) list -> theory -> thm list list * theory
val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory
- val note_thmss: string -> ((binding * attribute list) *
- (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
- val note_thmss_grouped: string -> string -> ((binding * attribute list) *
- (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
+ val note_thmss: string -> (Thm.binding *
+ (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
+ val note_thmss_grouped: string -> string -> (Thm.binding *
+ (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
val add_axioms: ((binding * term) * attribute list) list -> theory -> thm list * theory
val add_axioms_cmd: ((bstring * string) * attribute list) list -> theory -> thm list * theory
val add_defs: bool -> ((binding * term) * attribute list) list ->
@@ -151,14 +151,15 @@
fun enter_thms pre_name post_name app_att (b, thms) thy =
if Binding.is_empty b
then swap (enter_proofs (app_att (thy, thms)))
- else let
- val naming = Sign.naming_of thy;
- val name = NameSpace.full_name naming b;
- val (thy', thms') =
- enter_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
- val thms'' = map (Thm.transfer thy') thms';
- val thy'' = thy' |> (FactsData.map o apfst) (Facts.add_global naming (b, thms'') #> snd);
- in (thms'', thy'') end;
+ else
+ let
+ val naming = Sign.naming_of thy;
+ val name = NameSpace.full_name naming b;
+ val (thy', thms') =
+ enter_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
+ val thms'' = map (Thm.transfer thy') thms';
+ val thy'' = thy' |> (FactsData.map o apfst) (Facts.add_global naming (b, thms'') #> snd);
+ in (thms'', thy'') end;
(* store_thm(s) *)
--- a/src/Pure/sign.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/sign.ML Tue Mar 03 18:33:21 2009 +0100
@@ -507,12 +507,12 @@
val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt;
fun prep (raw_b, raw_T, raw_mx) =
let
- val (mx_name, mx) = Syntax.const_mixfix (Binding.base_name raw_b) raw_mx;
- val b = Binding.map_base (K mx_name) raw_b;
+ val (mx_name, mx) = Syntax.const_mixfix (Binding.name_of raw_b) raw_mx;
+ val b = Binding.map_name (K mx_name) raw_b;
val c = full_name thy b;
- val c_syn = if authentic then Syntax.constN ^ c else Binding.base_name b;
+ val c_syn = if authentic then Syntax.constN ^ c else Binding.name_of b;
val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
- cat_error msg ("in declaration of constant " ^ quote (Binding.display b));
+ cat_error msg ("in declaration of constant " ^ quote (Binding.str_of b));
val T' = Logic.varifyT T;
in ((b, T'), (c_syn, T', mx), Const (c, T)) end;
val args = map prep raw_args;
@@ -549,7 +549,7 @@
val pp = Syntax.pp_global thy;
val prep_tm = no_frees pp o Term.no_dummy_patterns o cert_term_abbrev thy;
val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
- handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.display b));
+ handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.str_of b));
val (res, consts') = consts_of thy
|> Consts.abbreviate pp (tsig_of thy) (naming_of thy) mode tags (b, t);
in (res, thy |> map_consts (K consts')) end;
--- a/src/Pure/theory.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/theory.ML Tue Mar 03 18:33:21 2009 +0100
@@ -258,7 +258,7 @@
val _ = check_overloading thy overloaded lhs_const;
in defs |> dependencies thy unchecked true name lhs_const rhs_consts end
handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
- [Pretty.str ("The error(s) above occurred in definition " ^ quote (Binding.display b) ^ ":"),
+ [Pretty.str ("The error(s) above occurred in definition " ^ quote (Binding.str_of b) ^ ":"),
Pretty.fbrk, Pretty.quote (Syntax.pretty_term_global thy tm)]));
--- a/src/Tools/induct.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Tools/induct.ML Tue Mar 03 18:33:21 2009 +0100
@@ -552,7 +552,7 @@
let
fun add (SOME (SOME x, t)) ctxt =
let val ([(lhs, (_, th))], ctxt') =
- LocalDefs.add_defs [((x, NoSyn), ((Binding.empty, []), t))] ctxt
+ LocalDefs.add_defs [((x, NoSyn), (Thm.empty_binding, t))] ctxt
in ((SOME lhs, [th]), ctxt') end
| add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt)
| add NONE ctxt = ((NONE, []), ctxt);
--- a/src/ZF/Tools/inductive_package.ML Tue Mar 03 17:05:18 2009 +0100
+++ b/src/ZF/Tools/inductive_package.ML Tue Mar 03 18:33:21 2009 +0100
@@ -65,7 +65,7 @@
val _ = Theory.requires thy "Inductive_ZF" "(co)inductive definitions";
val ctxt = ProofContext.init thy;
- val intr_specs = map (apfst (apfst Binding.base_name)) raw_intr_specs;
+ val intr_specs = map (apfst (apfst Binding.name_of)) raw_intr_specs;
val (intr_names, intr_tms) = split_list (map fst intr_specs);
val case_names = RuleCases.case_names intr_names;