# HG changeset patch
# User wenzelm
# Date 1256747893 -3600
# Node ID c6364889fea526dcd1dcb26e746064818c8e495c
# Parent  223ef9bc399ad1b1fe05019e296ef6d741143076
misc tuning;

diff -r 223ef9bc399a -r c6364889fea5 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Wed Oct 28 17:36:34 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Wed Oct 28 17:38:13 2009 +0100
@@ -181,9 +181,10 @@
     val similar_body = Type.similar_types (rhs, rhs');
     (* FIXME workaround based on educated guess *)
     val prefix' = Binding.prefix_of b';
-    val class_global = Binding.eq_name (b, b')
-      andalso not (null prefix')
-      andalso (fst o snd o split_last) prefix' = Class_Target.class_prefix target;
+    val class_global =
+      Binding.eq_name (b, b') andalso
+      not (null prefix') andalso
+      fst (snd (split_last prefix')) = Class_Target.class_prefix target;
   in
     not (is_class andalso (similar_body orelse class_global)) ?
       (Context.mapping_result
@@ -202,7 +203,7 @@
     val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
     val U = map #2 xs ---> T;
     val (mx1, mx2, mx3) = fork_mixfix ta mx;
-    val declare_const =
+    val (const, lthy') = lthy |>
       (case Class_Target.instantiation_param lthy b of
         SOME c' =>
           if mx3 <> NoSyn then syntax_error c'
@@ -215,7 +216,6 @@
                 else LocalTheory.theory_result (Overloading.declare (c', U))
                   ##> Overloading.confirm b
             | NONE => LocalTheory.theory_result (Sign.declare_const ((b, U), mx3))));
-    val (const, lthy') = lthy |> declare_const;
     val t = Term.list_comb (const, map Free xs);
   in
     lthy'
@@ -275,13 +275,13 @@
 
     (*def*)
     val (global_def, lthy3) = lthy2
-      |> LocalTheory.theory_result (case Overloading.operation lthy b of
-          SOME (_, checked) =>
-            Overloading.define checked name' ((fst o dest_Const) lhs', rhs')
+      |> LocalTheory.theory_result
+        (case Overloading.operation lthy b of
+          SOME (_, checked) => Overloading.define checked name' (fst (dest_Const lhs'), rhs')
         | NONE =>
             if is_none (Class_Target.instantiation_param lthy b)
             then Thm.add_def false false (name', Logic.mk_equals (lhs', rhs'))
-            else AxClass.define_overloaded name' ((fst o dest_Const) lhs', rhs'));
+            else AxClass.define_overloaded name' (fst (dest_Const lhs'), rhs'));
     val def = LocalDefs.trans_terms lthy3
       [(*c == global.c xs*)     local_def,
        (*global.c xs == rhs'*)  global_def,
@@ -341,6 +341,9 @@
 fun context "-" thy = init NONE thy
   | context target thy = init (SOME (Locale.intern thy target)) thy;
 
+
+(* other targets *)
+
 fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []);
 fun instantiation_cmd raw_arities thy =
   instantiation (Class_Target.read_multi_arity thy raw_arities) thy;