# HG changeset patch
# User haftmann
# Date 1281445659 -7200
# Node ID a1d63457a3c995c982125a657d11f5aeacee348b
# Parent  e7e84919392bc5477f7cd8b986fc234a72e70d8f
avoiding redundant primes

diff -r e7e84919392b -r a1d63457a3c9 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Tue Aug 10 14:57:58 2010 +0200
+++ b/src/Pure/Isar/theory_target.ML	Tue Aug 10 15:07:39 2010 +0200
@@ -122,37 +122,37 @@
 fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
 
 fun foundation (ta as Target {target, is_locale, is_class, ...})
-    (((b, U), mx), (b_def, rhs')) (type_params, term_params) lthy =
+    (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
   let
     val (mx1, mx2, mx3) = fork_mixfix ta mx;
     val (const, lthy2) = lthy |>
       (case Class_Target.instantiation_param lthy b of
-        SOME c' =>
-          if mx3 <> NoSyn then syntax_error c'
-          else Local_Theory.theory_result (AxClass.declare_overloaded (c', U))
+        SOME c =>
+          if mx3 <> NoSyn then syntax_error c
+          else Local_Theory.theory_result (AxClass.declare_overloaded (c, U))
             ##> Class_Target.confirm_declaration b
       | NONE =>
           (case Overloading.operation lthy b of
-            SOME (c', _) =>
-              if mx3 <> NoSyn then syntax_error c'
-              else Local_Theory.theory_result (Overloading.declare (c', U))
+            SOME (c, _) =>
+              if mx3 <> NoSyn then syntax_error c
+              else Local_Theory.theory_result (Overloading.declare (c, U))
                 ##> Overloading.confirm b
           | NONE => Local_Theory.theory_result (Sign.declare_const ((b, U), mx3))));
     val Const (head, _) = const;
-    val lhs' = list_comb (const, type_params @ term_params);
+    val lhs = list_comb (const, type_params @ term_params);
   in
     lthy2
-    |> pair lhs'
+    |> pair lhs
     ||>> Local_Theory.theory_result
       (case Overloading.operation lthy b of
-        SOME (_, checked) => Overloading.define checked b_def (head, rhs')
+        SOME (_, checked) => Overloading.define checked b_def (head, rhs)
       | NONE =>
           if is_some (Class_Target.instantiation_param lthy b)
-          then AxClass.define_overloaded b_def (head, rhs')
-          else Thm.add_def false false (b_def, Logic.mk_equals (lhs', rhs')) #>> snd)
-    ||> is_locale ? locale_const_declaration ta Syntax.mode_default ((b, mx2), lhs')
+          then AxClass.define_overloaded b_def (head, rhs)
+          else Thm.add_def false false (b_def, Logic.mk_equals (lhs, rhs)) #>> snd)
+    ||> is_locale ? locale_const_declaration ta Syntax.mode_default ((b, mx2), lhs)
     ||> is_class ? class_target ta
-          (Class_Target.declare target ((b, mx1), (type_params, lhs')))
+          (Class_Target.declare target ((b, mx1), (type_params, lhs)))
   end;
 
 in