misc tuning;
authorwenzelm
Wed Oct 28 17:38:13 2009 +0100 (2009-10-28)
changeset 33282c6364889fea5
parent 33281 223ef9bc399a
child 33283 810c16155233
misc tuning;
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/theory_target.ML	Wed Oct 28 17:36:34 2009 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Wed Oct 28 17:38:13 2009 +0100
     1.3 @@ -181,9 +181,10 @@
     1.4      val similar_body = Type.similar_types (rhs, rhs');
     1.5      (* FIXME workaround based on educated guess *)
     1.6      val prefix' = Binding.prefix_of b';
     1.7 -    val class_global = Binding.eq_name (b, b')
     1.8 -      andalso not (null prefix')
     1.9 -      andalso (fst o snd o split_last) prefix' = Class_Target.class_prefix target;
    1.10 +    val class_global =
    1.11 +      Binding.eq_name (b, b') andalso
    1.12 +      not (null prefix') andalso
    1.13 +      fst (snd (split_last prefix')) = Class_Target.class_prefix target;
    1.14    in
    1.15      not (is_class andalso (similar_body orelse class_global)) ?
    1.16        (Context.mapping_result
    1.17 @@ -202,7 +203,7 @@
    1.18      val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
    1.19      val U = map #2 xs ---> T;
    1.20      val (mx1, mx2, mx3) = fork_mixfix ta mx;
    1.21 -    val declare_const =
    1.22 +    val (const, lthy') = lthy |>
    1.23        (case Class_Target.instantiation_param lthy b of
    1.24          SOME c' =>
    1.25            if mx3 <> NoSyn then syntax_error c'
    1.26 @@ -215,7 +216,6 @@
    1.27                  else LocalTheory.theory_result (Overloading.declare (c', U))
    1.28                    ##> Overloading.confirm b
    1.29              | NONE => LocalTheory.theory_result (Sign.declare_const ((b, U), mx3))));
    1.30 -    val (const, lthy') = lthy |> declare_const;
    1.31      val t = Term.list_comb (const, map Free xs);
    1.32    in
    1.33      lthy'
    1.34 @@ -275,13 +275,13 @@
    1.35  
    1.36      (*def*)
    1.37      val (global_def, lthy3) = lthy2
    1.38 -      |> LocalTheory.theory_result (case Overloading.operation lthy b of
    1.39 -          SOME (_, checked) =>
    1.40 -            Overloading.define checked name' ((fst o dest_Const) lhs', rhs')
    1.41 +      |> LocalTheory.theory_result
    1.42 +        (case Overloading.operation lthy b of
    1.43 +          SOME (_, checked) => Overloading.define checked name' (fst (dest_Const lhs'), rhs')
    1.44          | NONE =>
    1.45              if is_none (Class_Target.instantiation_param lthy b)
    1.46              then Thm.add_def false false (name', Logic.mk_equals (lhs', rhs'))
    1.47 -            else AxClass.define_overloaded name' ((fst o dest_Const) lhs', rhs'));
    1.48 +            else AxClass.define_overloaded name' (fst (dest_Const lhs'), rhs'));
    1.49      val def = LocalDefs.trans_terms lthy3
    1.50        [(*c == global.c xs*)     local_def,
    1.51         (*global.c xs == rhs'*)  global_def,
    1.52 @@ -341,6 +341,9 @@
    1.53  fun context "-" thy = init NONE thy
    1.54    | context target thy = init (SOME (Locale.intern thy target)) thy;
    1.55  
    1.56 +
    1.57 +(* other targets *)
    1.58 +
    1.59  fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []);
    1.60  fun instantiation_cmd raw_arities thy =
    1.61    instantiation (Class_Target.read_multi_arity thy raw_arities) thy;