src/Pure/Isar/theory_target.ML
changeset 30519 c05c0199826f
parent 30473 e0b66c11e7e4
child 30761 ac7570d80c3d
     1.1 --- a/src/Pure/Isar/theory_target.ML	Fri Mar 13 19:17:57 2009 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Fri Mar 13 19:17:58 2009 +0100
     1.3 @@ -188,10 +188,7 @@
     1.4    in
     1.5      not (is_class andalso (similar_body orelse class_global)) ?
     1.6        (Context.mapping_result
     1.7 -        (fn thy => thy
     1.8 -          |> Sign.no_base_names
     1.9 -          |> Sign.add_abbrev PrintMode.internal tags legacy_arg
    1.10 -          ||> Sign.restore_naming thy)
    1.11 +        (Sign.add_abbrev PrintMode.internal tags legacy_arg)
    1.12          (ProofContext.add_abbrev PrintMode.internal tags arg)
    1.13        #-> (fn (lhs' as Const (d, _), _) =>
    1.14            similar_body ?
    1.15 @@ -203,23 +200,22 @@
    1.16  
    1.17  fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy =
    1.18    let
    1.19 -    val c = Binding.qualified_name_of b;
    1.20      val tags = LocalTheory.group_position_of lthy;
    1.21      val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
    1.22      val U = map #2 xs ---> T;
    1.23      val (mx1, mx2, mx3) = fork_mixfix ta mx;
    1.24      val declare_const =
    1.25 -      (case Class_Target.instantiation_param lthy c of
    1.26 +      (case Class_Target.instantiation_param lthy b of
    1.27          SOME c' =>
    1.28            if mx3 <> NoSyn then syntax_error c'
    1.29            else LocalTheory.theory_result (AxClass.declare_overloaded (c', U))
    1.30 -            ##> Class_Target.confirm_declaration c
    1.31 +            ##> Class_Target.confirm_declaration b
    1.32          | NONE =>
    1.33 -            (case Overloading.operation lthy c of
    1.34 +            (case Overloading.operation lthy b of
    1.35                SOME (c', _) =>
    1.36                  if mx3 <> NoSyn then syntax_error c'
    1.37                  else LocalTheory.theory_result (Overloading.declare (c', U))
    1.38 -                  ##> Overloading.confirm c
    1.39 +                  ##> Overloading.confirm b
    1.40              | NONE => LocalTheory.theory_result (Sign.declare_const tags ((b, U), mx3))));
    1.41      val (const, lthy') = lthy |> declare_const;
    1.42      val t = Term.list_comb (const, map Free xs);
    1.43 @@ -282,17 +278,14 @@
    1.44      val (_, lhs') = Logic.dest_equals (Thm.prop_of local_def);
    1.45  
    1.46      (*def*)
    1.47 -    val c = Binding.qualified_name_of b;
    1.48 -    val define_const =
    1.49 -      (case Overloading.operation lthy c of
    1.50 -        SOME (_, checked) =>
    1.51 -          (fn name => fn (Const (c, _), rhs) => Overloading.define checked name (c, rhs))
    1.52 -      | NONE =>
    1.53 -          if is_none (Class_Target.instantiation_param lthy c)
    1.54 -          then (fn name => fn eq => Thm.add_def false false (Binding.name name, Logic.mk_equals eq))
    1.55 -          else (fn name => fn (Const (c, _), rhs) => AxClass.define_overloaded name (c, rhs)));
    1.56      val (global_def, lthy3) = lthy2
    1.57 -      |> LocalTheory.theory_result (define_const (Binding.name_of name') (lhs', rhs'));
    1.58 +      |> LocalTheory.theory_result (case Overloading.operation lthy b of
    1.59 +          SOME (_, checked) =>
    1.60 +            Overloading.define checked name' ((fst o dest_Const) lhs', rhs')
    1.61 +        | NONE =>
    1.62 +            if is_none (Class_Target.instantiation_param lthy b)
    1.63 +            then Thm.add_def false false (name', Logic.mk_equals (lhs', rhs'))
    1.64 +            else AxClass.define_overloaded name' ((fst o dest_Const) lhs', rhs'));
    1.65      val def = LocalDefs.trans_terms lthy3
    1.66        [(*c == global.c xs*)     local_def,
    1.67         (*global.c xs == rhs'*)  global_def,