src/Pure/tactic.ML
changeset 29276 94b1ffec9201
parent 27243 d549b5b0f344
child 30558 2ef9892114fd
     1.1 --- a/src/Pure/tactic.ML	Wed Dec 31 18:53:19 2008 +0100
     1.2 +++ b/src/Pure/tactic.ML	Wed Dec 31 19:54:03 2008 +0100
     1.3 @@ -1,9 +1,7 @@
     1.4  (*  Title:      Pure/tactic.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1991  University of Cambridge
     1.8  
     1.9 -Basic tactics.
    1.10 +Fundamental tactics.
    1.11  *)
    1.12  
    1.13  signature BASIC_TACTIC =
    1.14 @@ -192,7 +190,7 @@
    1.15  (*Determine print names of goal parameters (reversed)*)
    1.16  fun innermost_params i st =
    1.17    let val (_, _, Bi, _) = dest_state (st, i)
    1.18 -  in rename_wrt_term Bi (Logic.strip_params Bi) end;
    1.19 +  in Term.rename_wrt_term Bi (Logic.strip_params Bi) end;
    1.20  
    1.21  (*params of subgoal i as they are printed*)
    1.22  fun params_of_state i st = rev (innermost_params i st);