--- a/src/Pure/Isar/theory_target.ML Wed Mar 11 15:44:12 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML Wed Mar 11 15:45:40 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]);
@@ -195,8 +196,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 +211,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 +279,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 +290,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) =>