Removed Logic.auto_rename.
authorberghofe
Mon Jan 21 14:18:49 2008 +0100 (2008-01-21)
changeset 25939ddea202704b4
parent 25938 2c1c0e989615
child 25940 6942f3c5dec8
Removed Logic.auto_rename.
src/HOL/ex/Meson_Test.thy
src/Pure/logic.ML
src/Pure/tactic.ML
src/Pure/thm.ML
     1.1 --- a/src/HOL/ex/Meson_Test.thy	Mon Jan 21 08:45:36 2008 +0100
     1.2 +++ b/src/HOL/ex/Meson_Test.thy	Mon Jan 21 14:18:49 2008 +0100
     1.3 @@ -22,9 +22,6 @@
     1.4  
     1.5  subsection {* Interactive examples *}
     1.6  
     1.7 -(*Generate nice names for Skolem functions*)
     1.8 -ML {* Logic.auto_rename := true; Logic.set_rename_prefix "a" *}
     1.9 -
    1.10  ML {*
    1.11  writeln"Problem 25";
    1.12  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)";
    1.13 @@ -86,8 +83,6 @@
    1.14  by (Meson.best_prolog_tac Meson.size_of_subgoals horns43);   (*1.6 secs*)
    1.15  *}
    1.16  
    1.17 -ML {* Logic.auto_rename := false; *}
    1.18 -
    1.19  (*
    1.20  #1  (q x xa ==> ~ q x xa) ==> q xa x
    1.21  #2  (q xa x ==> ~ q xa x) ==> q x xa
     2.1 --- a/src/Pure/logic.ML	Mon Jan 21 08:45:36 2008 +0100
     2.2 +++ b/src/Pure/logic.ML	Mon Jan 21 14:18:49 2008 +0100
     2.3 @@ -61,8 +61,6 @@
     2.4    val strip_params: term -> (string * typ) list
     2.5    val has_meta_prems: term -> bool
     2.6    val flatten_params: int -> term -> term
     2.7 -  val auto_rename: bool ref
     2.8 -  val set_rename_prefix: string -> unit
     2.9    val list_rename_params: string list * term -> term
    2.10    val assum_pairs: int * term -> (term*term)list
    2.11    val varifyT: typ -> typ
    2.12 @@ -398,32 +396,12 @@
    2.13        | _ => if n>0 then raise TERM("remove_params", [A])
    2.14               else A;
    2.15  
    2.16 -(** Auto-renaming of parameters in subgoals **)
    2.17 -
    2.18 -val auto_rename = ref false
    2.19 -and rename_prefix = ref "ka";
    2.20 -
    2.21 -(*rename_prefix is not exported; it is set by this function.*)
    2.22 -fun set_rename_prefix a =
    2.23 -    if a<>"" andalso forall Symbol.is_letter (Symbol.explode a)
    2.24 -    then  (rename_prefix := a;  auto_rename := true)
    2.25 -    else  error"rename prefix must be nonempty and consist of letters";
    2.26 -
    2.27 -(*Makes parameters in a goal have distinctive names (not guaranteed unique!)
    2.28 -  A name clash could cause the printer to rename bound vars;
    2.29 -    then res_inst_tac would not work properly.*)
    2.30 -fun rename_vars (a, []) = []
    2.31 -  | rename_vars (a, (_,T)::vars) =
    2.32 -        (a,T) :: rename_vars (Symbol.bump_string a, vars);
    2.33 -
    2.34  (*Move all parameters to the front of the subgoal, renaming them apart;
    2.35    if n>0 then deletes assumption n. *)
    2.36  fun flatten_params n A =
    2.37      let val params = strip_params A;
    2.38 -        val vars = if !auto_rename
    2.39 -                   then rename_vars (!rename_prefix, params)
    2.40 -                   else ListPair.zip (Name.variant_list [] (map #1 params),
    2.41 -                                      map #2 params)
    2.42 +        val vars = ListPair.zip (Name.variant_list [] (map #1 params),
    2.43 +                                 map #2 params)
    2.44      in  list_all (vars, remove_params (length vars) n A)
    2.45      end;
    2.46  
     3.1 --- a/src/Pure/tactic.ML	Mon Jan 21 08:45:36 2008 +0100
     3.2 +++ b/src/Pure/tactic.ML	Mon Jan 21 14:18:49 2008 +0100
     3.3 @@ -506,11 +506,7 @@
     3.4  fun rename_params_tac xs i =
     3.5    case Library.find_first (not o Syntax.is_identifier) xs of
     3.6        SOME x => error ("Not an identifier: " ^ x)
     3.7 -    | NONE =>
     3.8 -       (if !Logic.auto_rename
     3.9 -         then (warning "Resetting Logic.auto_rename";
    3.10 -             Logic.auto_rename := false)
    3.11 -        else (); PRIMITIVE (rename_params_rule (xs, i)));
    3.12 +    | NONE => PRIMITIVE (rename_params_rule (xs, i));
    3.13  
    3.14  (*scan a list of characters into "words" composed of "letters" (recognized by
    3.15    is_let) and separated by any number of non-"letters"*)
     4.1 --- a/src/Pure/thm.ML	Mon Jan 21 08:45:36 2008 +0100
     4.2 +++ b/src/Pure/thm.ML	Mon Jan 21 14:18:49 2008 +0100
     4.3 @@ -1544,7 +1544,7 @@
     4.4       (*Modify assumptions, deleting n-th if n>0 for e-resolution*)
     4.5       fun newAs(As0, n, dpairs, tpairs) =
     4.6         let val (As1, rder') =
     4.7 -         if !Logic.auto_rename orelse not lifted then (As0, rder)
     4.8 +         if not lifted then (As0, rder)
     4.9           else (map (rename_bvars(dpairs,tpairs,B)) As0,
    4.10             Pt.infer_derivs' (Pt.map_proof_terms
    4.11               (rename_bvars (dpairs, tpairs, Bound 0)) I) rder);