more precise treatment of qualified bindings;
authorwenzelm
Wed Mar 11 15:45:40 2009 +0100 (2009-03-11)
changeset 30437910a7aeb8dec
parent 30436 0e3c88f132fc
child 30438 c2d49315b93b
more precise treatment of qualified bindings;
tuned;
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/theory_target.ML	Wed Mar 11 15:44:12 2009 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Wed Mar 11 15:45:40 2009 +0100
     1.3 @@ -1,5 +1,6 @@
     1.4  (*  Title:      Pure/Isar/theory_target.ML
     1.5      Author:     Makarius
     1.6 +    Author:     Florian Haftmann, TU Muenchen
     1.7  
     1.8  Common theory/locale/class/instantiation/overloading targets.
     1.9  *)
    1.10 @@ -48,10 +49,10 @@
    1.11    let
    1.12      val thy = ProofContext.theory_of ctxt;
    1.13      val target_name = (if is_class then "class " else "locale ") ^ Locale.extern thy target;
    1.14 -    val fixes = map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
    1.15 -      (#1 (ProofContext.inferred_fixes ctxt));
    1.16 -    val assumes = map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
    1.17 -      (Assumption.assms_of ctxt);
    1.18 +    val fixes =
    1.19 +      map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt));
    1.20 +    val assumes =
    1.21 +      map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])])) (Assumption.assms_of ctxt);
    1.22      val elems =
    1.23        (if null fixes then [] else [Element.Fixes fixes]) @
    1.24        (if null assumes then [] else [Element.Assumes assumes]);
    1.25 @@ -195,8 +196,8 @@
    1.26    in
    1.27      not (is_class andalso (similar_body orelse class_global)) ?
    1.28        (Context.mapping_result
    1.29 -        (fn thy => thy |> 
    1.30 -          Sign.no_base_names
    1.31 +        (fn thy => thy
    1.32 +          |> Sign.no_base_names
    1.33            |> Sign.add_abbrev PrintMode.internal tags legacy_arg
    1.34            ||> Sign.restore_naming thy)
    1.35          (ProofContext.add_abbrev PrintMode.internal tags arg)
    1.36 @@ -210,7 +211,7 @@
    1.37  
    1.38  fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy =
    1.39    let
    1.40 -    val c = Binding.name_of b;  (* FIXME Binding.qualified_name_of *)
    1.41 +    val c = Binding.qualified_name_of b;
    1.42      val tags = LocalTheory.group_position_of lthy;
    1.43      val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
    1.44      val U = map #2 xs ---> T;
    1.45 @@ -278,8 +279,7 @@
    1.46      val thy = ProofContext.theory_of lthy;
    1.47      val thy_ctxt = ProofContext.init thy;
    1.48  
    1.49 -    val c = Binding.name_of b;   (* FIXME Binding.qualified_name_of (!?) *)
    1.50 -    val name' = Binding.map_name (Thm.def_name_optional (Binding.name_of b)) name;
    1.51 +    val name' = Thm.def_binding_optional b name;
    1.52      val (rhs', rhs_conv) =
    1.53        LocalDefs.export_cterm lthy thy_ctxt (Thm.cterm_of thy rhs) |>> Thm.term_of;
    1.54      val xs = Variable.add_fixed (LocalTheory.target_of lthy) rhs' [];
    1.55 @@ -290,6 +290,7 @@
    1.56      val (_, lhs') = Logic.dest_equals (Thm.prop_of local_def);
    1.57  
    1.58      (*def*)
    1.59 +    val c = Binding.qualified_name_of b;
    1.60      val define_const =
    1.61        (case Overloading.operation lthy c of
    1.62          SOME (_, checked) =>