--- a/src/Pure/Isar/element.ML Tue Mar 03 18:31:59 2009 +0100
+++ b/src/Pure/Isar/element.ML Tue Mar 03 18:32:01 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)) =>
@@ -143,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))
@@ -168,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);
@@ -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_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);
@@ -527,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,