src/Pure/Isar/theory_target.ML
changeset 29006 abe0f11cfa4e
parent 28991 694227dd3e8c
child 29102 2e1011dcd577
child 29223 e09c53289830
     1.1 --- a/src/Pure/Isar/theory_target.ML	Fri Dec 05 18:42:39 2008 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Fri Dec 05 18:43:42 2008 +0100
     1.3 @@ -200,7 +200,7 @@
     1.4      val similar_body = Type.similar_types (rhs, rhs');
     1.5      (* FIXME workaround based on educated guess *)
     1.6      val (prefix', _) = Binding.dest b';
     1.7 -    val class_global = Name.name_of b = Name.name_of b'
     1.8 +    val class_global = Binding.base_name b = Binding.base_name b'
     1.9        andalso not (null prefix')
    1.10        andalso (fst o snd o split_last) prefix' = Class.class_prefix target;
    1.11    in
    1.12 @@ -219,7 +219,7 @@
    1.13  
    1.14  fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy =
    1.15    let
    1.16 -    val c = Name.name_of b;
    1.17 +    val c = Binding.base_name b;
    1.18      val tags = LocalTheory.group_position_of lthy;
    1.19      val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
    1.20      val U = map #2 xs ---> T;
    1.21 @@ -252,7 +252,7 @@
    1.22  
    1.23  fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((b, mx), t) lthy =
    1.24    let
    1.25 -    val c = Name.name_of b;
    1.26 +    val c = Binding.base_name b;
    1.27      val tags = LocalTheory.group_position_of lthy;
    1.28      val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
    1.29      val target_ctxt = LocalTheory.target_of lthy;
    1.30 @@ -289,7 +289,7 @@
    1.31      val thy = ProofContext.theory_of lthy;
    1.32      val thy_ctxt = ProofContext.init thy;
    1.33  
    1.34 -    val c = Name.name_of b;
    1.35 +    val c = Binding.base_name b;
    1.36      val name' = Binding.map_base (Thm.def_name_optional c) name;
    1.37      val (rhs', rhs_conv) =
    1.38        LocalDefs.export_cterm lthy thy_ctxt (Thm.cterm_of thy rhs) |>> Thm.term_of;
    1.39 @@ -310,7 +310,7 @@
    1.40            then (fn name => fn eq => Thm.add_def false false (name, Logic.mk_equals eq))
    1.41            else (fn name => fn (Const (c, _), rhs) => AxClass.define_overloaded name (c, rhs)));
    1.42      val (global_def, lthy3) = lthy2
    1.43 -      |> LocalTheory.theory_result (define_const (Name.name_of name') (lhs', rhs'));
    1.44 +      |> LocalTheory.theory_result (define_const (Binding.base_name name') (lhs', rhs'));
    1.45      val def = LocalDefs.trans_terms lthy3
    1.46        [(*c == global.c xs*)     local_def,
    1.47         (*global.c xs == rhs'*)  global_def,