src/Pure/logic.ML
changeset 29276 94b1ffec9201
parent 28856 5e009a80fe6d
child 30280 eb98b49ef835
     1.1 --- a/src/Pure/logic.ML	Wed Dec 31 18:53:19 2008 +0100
     1.2 +++ b/src/Pure/logic.ML	Wed Dec 31 19:54:03 2008 +0100
     1.3 @@ -1,7 +1,6 @@
     1.4  (*  Title:      Pure/logic.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   Cambridge University 1992
     1.8 +    Author:     Makarius
     1.9  
    1.10  Abstract syntax operations of the Pure meta-logic.
    1.11  *)
    1.12 @@ -515,7 +514,7 @@
    1.13  (*reverses parameters for substitution*)
    1.14  fun goal_params st i =
    1.15    let val gi = get_goal st i
    1.16 -      val rfrees = map Free (rename_wrt_term gi (strip_params gi))
    1.17 +      val rfrees = map Free (Term.rename_wrt_term gi (strip_params gi))
    1.18    in (gi, rfrees) end;
    1.19  
    1.20  fun concl_of_goal st i =