# HG changeset patch
# User haftmann
# Date 1401297452 -7200
# Node ID 84c1e0453bda3be964dc744bb365122a95d2c059
# Parent  dc0b4f50e288831c9a1eaf14b604ab7fac6aa6fa
tuned variable names

diff -r dc0b4f50e288 -r 84c1e0453bda src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed May 28 17:42:36 2014 +0200
+++ b/src/Pure/Isar/class.ML	Wed May 28 19:17:32 2014 +0200
@@ -391,9 +391,9 @@
   class_const class Syntax.mode_default (b, lhs)
   #> target_extension (global_const params) class ((b, mx), lhs);
 
-fun abbrev class prmode ((b, mx), lhs) t' =
+fun abbrev class prmode ((b, mx), lhs) rhs' =
   class_const class prmode (b, lhs)
-  #> target_extension (global_abbrev prmode) class ((b, mx), t');
+  #> target_extension (global_abbrev prmode) class ((b, mx), rhs');
 
 end;
 
diff -r dc0b4f50e288 -r 84c1e0453bda src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Wed May 28 17:42:36 2014 +0200
+++ b/src/Pure/Isar/generic_target.ML	Wed May 28 19:17:32 2014 +0200
@@ -198,17 +198,17 @@
 
 (* abbrev *)
 
-fun background_abbrev (b, t) xs =
-  Local_Theory.background_theory_result (Sign.add_abbrev Print_Mode.internal (b, t))
-  #>> (fn (lhs, rhs) => (Term.list_comb (Logic.unvarify_global lhs, xs), rhs))
+fun background_abbrev (b, global_rhs) params =
+  Local_Theory.background_theory_result (Sign.add_abbrev Print_Mode.internal (b, global_rhs))
+  #>> (fn (lhs, rhs) => (Term.list_comb (Logic.unvarify_global lhs, params), rhs))
 
-fun abbrev target_abbrev prmode ((b, mx), t) lthy =
+fun abbrev target_abbrev prmode ((b, mx), rhs) lthy =
   let
     val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
 
-    val t' = Assumption.export_term lthy (Local_Theory.target_of lthy) t;
-    val xs = map Free (sort (Variable.fixed_ord lthy o pairself #1) (Variable.add_fixed lthy t' []));
-    val u = fold_rev lambda xs t';
+    val rhs' = Assumption.export_term lthy (Local_Theory.target_of lthy) rhs;
+    val params = map Free (sort (Variable.fixed_ord lthy o pairself #1) (Variable.add_fixed lthy rhs' []));
+    val u = fold_rev lambda params rhs';
     val global_rhs = singleton (Variable.polymorphic thy_ctxt) u;
 
     val extra_tfrees =
@@ -216,9 +216,9 @@
     val mx' = check_mixfix lthy (b, extra_tfrees) mx;
   in
     lthy
-    |> target_abbrev prmode (b, mx') (global_rhs, t') xs
-    |> Proof_Context.add_abbrev Print_Mode.internal (b, t) |> snd
-    |> Local_Defs.fixed_abbrev ((b, NoSyn), t)
+    |> target_abbrev prmode (b, mx') (global_rhs, rhs') params
+    |> Proof_Context.add_abbrev Print_Mode.internal (b, rhs) |> snd
+    |> Local_Defs.fixed_abbrev ((b, NoSyn), rhs)
   end;
 
 
@@ -331,13 +331,13 @@
       ctxt |> Attrib.local_notes kind
         (Element.transform_facts (Local_Theory.standard_morphism lthy ctxt) local_facts) |> snd));
 
-fun theory_abbrev prmode (b, mx) (t, _) xs =
+fun theory_abbrev prmode (b, mx) (global_rhs, _) params =
   Local_Theory.background_theory_result
-    (Sign.add_abbrev (#1 prmode) (b, t) #->
+    (Sign.add_abbrev (#1 prmode) (b, global_rhs) #->
       (fn (lhs, _) =>  (* FIXME type_params!? *)
-        Sign.notation true prmode [(lhs, check_mixfix_global (b, null xs) mx)] #> pair lhs))
+        Sign.notation true prmode [(lhs, check_mixfix_global (b, null params) mx)] #> pair lhs))
   #-> (fn lhs => const (op <>) prmode
-          ((b, if null xs then NoSyn else mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
+          ((b, if null params then NoSyn else mx), Term.list_comb (Logic.unvarify_global lhs, params)));
 
 fun theory_declaration decl =
   background_declaration decl #> standard_declaration (K true) decl;
diff -r dc0b4f50e288 -r 84c1e0453bda src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Wed May 28 17:42:36 2014 +0200
+++ b/src/Pure/Isar/named_target.ML	Wed May 28 19:17:32 2014 +0200
@@ -75,13 +75,13 @@
 
 (* abbrev *)
 
-fun locale_abbrev locale prmode (b, mx) (t, _) xs =
-  Generic_Target.background_abbrev (b, t) xs
+fun locale_abbrev locale prmode (b, mx) (global_rhs, _) params =
+  Generic_Target.background_abbrev (b, global_rhs) params
   #-> (fn (lhs, _) => Generic_Target.locale_const locale prmode ((b, mx), lhs));
 
-fun class_abbrev class prmode (b, mx) (t, t') xs =
-  Generic_Target.background_abbrev (b, t) xs
-  #-> (fn (lhs, _) => Class.abbrev class prmode ((b, mx), lhs) t');
+fun class_abbrev class prmode (b, mx) (global_rhs, rhs') params =
+  Generic_Target.background_abbrev (b, global_rhs) params
+  #-> (fn (lhs, _) => Class.abbrev class prmode ((b, mx), lhs) rhs');
 
 fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) =
   if is_class then class_abbrev target