# HG changeset patch
# User berghofe
# Date 1200921529 -3600
# Node ID ddea202704b4813210fc8ae32de73bd4a3c0ccd7
# Parent  2c1c0e9896158bce5ee9e0a263777158e5337cb2
Removed Logic.auto_rename.

diff -r 2c1c0e989615 -r ddea202704b4 src/HOL/ex/Meson_Test.thy
--- a/src/HOL/ex/Meson_Test.thy	Mon Jan 21 08:45:36 2008 +0100
+++ b/src/HOL/ex/Meson_Test.thy	Mon Jan 21 14:18:49 2008 +0100
@@ -22,9 +22,6 @@
 
 subsection {* Interactive examples *}
 
-(*Generate nice names for Skolem functions*)
-ML {* Logic.auto_rename := true; Logic.set_rename_prefix "a" *}
-
 ML {*
 writeln"Problem 25";
 Goal "(\<exists>x. P x) & (\<forall>x. L x --> ~ (M x & R x)) & (\<forall>x. P x --> (M x & L x)) & ((\<forall>x. P x --> Q x) | (\<exists>x. P x & R x)) --> (\<exists>x. Q x & P x)";
@@ -86,8 +83,6 @@
 by (Meson.best_prolog_tac Meson.size_of_subgoals horns43);   (*1.6 secs*)
 *}
 
-ML {* Logic.auto_rename := false; *}
-
 (*
 #1  (q x xa ==> ~ q x xa) ==> q xa x
 #2  (q xa x ==> ~ q xa x) ==> q x xa
diff -r 2c1c0e989615 -r ddea202704b4 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Mon Jan 21 08:45:36 2008 +0100
+++ b/src/Pure/logic.ML	Mon Jan 21 14:18:49 2008 +0100
@@ -61,8 +61,6 @@
   val strip_params: term -> (string * typ) list
   val has_meta_prems: term -> bool
   val flatten_params: int -> term -> term
-  val auto_rename: bool ref
-  val set_rename_prefix: string -> unit
   val list_rename_params: string list * term -> term
   val assum_pairs: int * term -> (term*term)list
   val varifyT: typ -> typ
@@ -398,32 +396,12 @@
       | _ => if n>0 then raise TERM("remove_params", [A])
              else A;
 
-(** Auto-renaming of parameters in subgoals **)
-
-val auto_rename = ref false
-and rename_prefix = ref "ka";
-
-(*rename_prefix is not exported; it is set by this function.*)
-fun set_rename_prefix a =
-    if a<>"" andalso forall Symbol.is_letter (Symbol.explode a)
-    then  (rename_prefix := a;  auto_rename := true)
-    else  error"rename prefix must be nonempty and consist of letters";
-
-(*Makes parameters in a goal have distinctive names (not guaranteed unique!)
-  A name clash could cause the printer to rename bound vars;
-    then res_inst_tac would not work properly.*)
-fun rename_vars (a, []) = []
-  | rename_vars (a, (_,T)::vars) =
-        (a,T) :: rename_vars (Symbol.bump_string a, vars);
-
 (*Move all parameters to the front of the subgoal, renaming them apart;
   if n>0 then deletes assumption n. *)
 fun flatten_params n A =
     let val params = strip_params A;
-        val vars = if !auto_rename
-                   then rename_vars (!rename_prefix, params)
-                   else ListPair.zip (Name.variant_list [] (map #1 params),
-                                      map #2 params)
+        val vars = ListPair.zip (Name.variant_list [] (map #1 params),
+                                 map #2 params)
     in  list_all (vars, remove_params (length vars) n A)
     end;
 
diff -r 2c1c0e989615 -r ddea202704b4 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Mon Jan 21 08:45:36 2008 +0100
+++ b/src/Pure/tactic.ML	Mon Jan 21 14:18:49 2008 +0100
@@ -506,11 +506,7 @@
 fun rename_params_tac xs i =
   case Library.find_first (not o Syntax.is_identifier) xs of
       SOME x => error ("Not an identifier: " ^ x)
-    | NONE =>
-       (if !Logic.auto_rename
-         then (warning "Resetting Logic.auto_rename";
-             Logic.auto_rename := false)
-        else (); PRIMITIVE (rename_params_rule (xs, i)));
+    | NONE => PRIMITIVE (rename_params_rule (xs, i));
 
 (*scan a list of characters into "words" composed of "letters" (recognized by
   is_let) and separated by any number of non-"letters"*)
diff -r 2c1c0e989615 -r ddea202704b4 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Jan 21 08:45:36 2008 +0100
+++ b/src/Pure/thm.ML	Mon Jan 21 14:18:49 2008 +0100
@@ -1544,7 +1544,7 @@
      (*Modify assumptions, deleting n-th if n>0 for e-resolution*)
      fun newAs(As0, n, dpairs, tpairs) =
        let val (As1, rder') =
-         if !Logic.auto_rename orelse not lifted then (As0, rder)
+         if not lifted then (As0, rder)
          else (map (rename_bvars(dpairs,tpairs,B)) As0,
            Pt.infer_derivs' (Pt.map_proof_terms
              (rename_bvars (dpairs, tpairs, Bound 0)) I) rder);