# HG changeset patch
# User huffman
# Date 1268519186 28800
# Node ID ea0ac5538c53664840a7cd9450aac64698b2d7c8
# Parent  2b75230f272fa2e0e1a6d3d2d3283d441f64eedd
avoid unnecessary primed variable names

diff -r 2b75230f272f -r ea0ac5538c53 src/HOLCF/Tools/fixrec.ML
--- a/src/HOLCF/Tools/fixrec.ML	Sat Mar 13 12:24:50 2010 -0800
+++ b/src/HOLCF/Tools/fixrec.ML	Sat Mar 13 14:26:26 2010 -0800
@@ -138,7 +138,7 @@
       | defs (l::[]) r = [one_def l r]
       | defs (l::ls) r = one_def l (mk_fst r) :: defs ls (mk_snd r);
     val fixdefs = defs lhss fixpoint;
-    val (fixdef_thms : (term * (string * thm)) list, lthy') = lthy
+    val (fixdef_thms : (term * (string * thm)) list, lthy) = lthy
       |> fold_map Local_Theory.define (map (apfst fst) fixes ~~ fixdefs);
     fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2];
     val tuple_fixdef_thm = foldr1 pair_equalI (map (snd o snd) fixdef_thms);
@@ -148,7 +148,7 @@
       |> Drule.instantiate' [] [SOME (Thm.cterm_of thy predicate)]
       |> Local_Defs.unfold lthy @{thms split_paired_all split_conv split_strict};
     val tuple_unfold_thm = (def_cont_fix_eq OF [tuple_fixdef_thm, cont_thm])
-      |> Local_Defs.unfold lthy' @{thms split_conv};
+      |> Local_Defs.unfold lthy @{thms split_conv};
     fun unfolds [] thm = []
       | unfolds (n::[]) thm = [(n, thm)]
       | unfolds (n::ns) thm = let
@@ -169,10 +169,10 @@
       in
         ((thm_name, [src]), [thm])
       end;
-    val (thmss, lthy'') = lthy'
+    val (thmss, lthy) = lthy
       |> fold_map Local_Theory.note (induct_note :: map unfold_note unfold_thms);
   in
-    (lthy'', names, fixdef_thms, map snd unfold_thms)
+    (lthy, names, fixdef_thms, map snd unfold_thms)
   end;
 
 (*************************************************************************)
@@ -377,12 +377,12 @@
 
     val matches = map (compile_pats match_name) (map (map snd) blocks);
     val spec' = map (pair Attrib.empty_binding) matches;
-    val (lthy', cnames, fixdef_thms, unfold_thms) =
+    val (lthy, cnames, fixdef_thms, unfold_thms) =
       add_fixdefs fixes spec' lthy;
   in
     if strict then let (* only prove simp rules if strict = true *)
       val simps : (Attrib.binding * thm) list list =
-        map (make_simps lthy') (unfold_thms ~~ blocks);
+        map (make_simps lthy) (unfold_thms ~~ blocks);
       fun mk_bind n : Attrib.binding =
        (Binding.qualify true n (Binding.name "simps"),
          [Attrib.internal (K Simplifier.simp_add)]);
@@ -390,12 +390,12 @@
         map (fn (n,xs) => (mk_bind n, map snd xs)) (names ~~ simps);
       val simps2 : (Attrib.binding * thm list) list =
         map (apsnd (fn thm => [thm])) (flat simps);
-      val (_, lthy'') = lthy'
+      val (_, lthy) = lthy
         |> fold_map Local_Theory.note (simps1 @ simps2);
     in
-      lthy''
+      lthy
     end
-    else lthy'
+    else lthy
   end;
 
 in